class LO.Modal.Neighborhood.Frame.IsEND4 (F : Frame) extends F.IsEND, F.IsTransitive : Prop

• contains_unit : F.box Set.univ = Set.univ
• serial (X : Set F.World) : F.box X ⊆ F.dia X
• trans (X : Set F.World) : F.box X ⊆ F.box^[2] X

@[reducible, inline]

abbrev LO.Modal.Neighborhood.FrameClass.END4 : FrameClass

Equations

• LO.Modal.Neighborhood.FrameClass.END4 = {F : LO.Modal.Neighborhood.Frame | F.IsEND4}

instance LO.Modal.Neighborhood.instIsENDCounterframe_2_3_5 : counterframe_2_3_5.IsEND

instance LO.Modal.END4.instSoundLogicNatFormulaFrameClassEND4 : Sound Modal.END4 Neighborhood.FrameClass.END4

instance LO.Modal.END4.instConsistentFormulaNatLogic : Entailment.Consistent Modal.END4

instance LO.Modal.instStrictlyWeakerThanFormulaNatLogicENDEND4 : Modal.END ⪱ Modal.END4