:: OPOSET_1 semantic presentation begin theorem :: OPOSET_1:1 for L being non empty reflexive antisymmetric RelStr for x, y being Element of L st x <= y holds ( sup {x,y} = y & inf {x,y} = x ) proof let R be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of R st x <= y holds ( sup {x,y} = y & inf {x,y} = x ) let a, b be Element of R; ::_thesis: ( a <= b implies ( sup {a,b} = b & inf {a,b} = a ) ) A1: for x being Element of R st x is_>=_than {a,b} holds b <= x proof let a0 be Element of R; ::_thesis: ( a0 is_>=_than {a,b} implies b <= a0 ) A2: b in {a,b} by TARSKI:def_2; assume a0 is_>=_than {a,b} ; ::_thesis: b <= a0 hence b <= a0 by A2, LATTICE3:def_9; ::_thesis: verum end; A3: for x being Element of R st x is_<=_than {a,b} holds a >= x proof let a0 be Element of R; ::_thesis: ( a0 is_<=_than {a,b} implies a >= a0 ) A4: a in {a,b} by TARSKI:def_2; assume a0 is_<=_than {a,b} ; ::_thesis: a >= a0 hence a >= a0 by A4, LATTICE3:def_8; ::_thesis: verum end; assume A5: a <= b ; ::_thesis: ( sup {a,b} = b & inf {a,b} = a ) for x being Element of {a,b} holds x >= a proof let a0 be Element of {a,b}; ::_thesis: a0 >= a ( a <= a0 or a <= a0 ) by A5, TARSKI:def_2; hence a0 >= a ; ::_thesis: verum end; then for x being Element of R st x in {a,b} holds x >= a ; then A6: a is_<=_than {a,b} by LATTICE3:def_8; for x being Element of R st x in {a,b} holds x <= b by A5, TARSKI:def_2; then b is_>=_than {a,b} by LATTICE3:def_9; hence ( sup {a,b} = b & inf {a,b} = a ) by A6, A1, A3, YELLOW_0:30, YELLOW_0:31; ::_thesis: verum end; registration let X be set ; cluster Relation-like irreflexive asymmetric transitive for Element of K19(([#] (X,X))); existence ex b1 being Relation of X st ( b1 is irreflexive & b1 is asymmetric & b1 is transitive ) proof {} (X,X) = {} ; hence ex b1 being Relation of X st ( b1 is irreflexive & b1 is asymmetric & b1 is transitive ) ; ::_thesis: verum end; end; registration let X be non empty set ; let R be Relation of X; let C be UnOp of X; cluster OrthoRelStr(# X,R,C #) -> non empty ; coherence not OrthoRelStr(# X,R,C #) is empty ; end; registration cluster non empty strict for OrthoRelStr ; existence ex b1 being OrthoRelStr st ( not b1 is empty & b1 is strict ) proof set X = the non empty set ; set R = the Relation of the non empty set ; set C = the UnOp of the non empty set ; take OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) ; ::_thesis: ( not OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is empty & OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is strict ) thus ( not OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is empty & OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is strict ) ; ::_thesis: verum end; end; registration let O be set ; cluster Relation-like Function-like V14(O) V18(O,O) involutive for Element of K19(([#] (O,O))); existence ex b1 being Function of O,O st b1 is involutive proof take id O ; ::_thesis: id O is involutive thus id O is involutive ; ::_thesis: verum end; end; definition func TrivOrthoRelStr -> strict OrthoRelStr equals :Def1: :: OPOSET_1:def 1 OrthoRelStr(# 1,(id 1),op1 #); coherence OrthoRelStr(# 1,(id 1),op1 #) is strict OrthoRelStr ; end; :: deftheorem Def1 defines TrivOrthoRelStr OPOSET_1:def_1_:_ TrivOrthoRelStr = OrthoRelStr(# 1,(id 1),op1 #); notation synonym TrivPoset for TrivOrthoRelStr ; end; registration cluster TrivOrthoRelStr -> 1 -element strict ; coherence TrivOrthoRelStr is 1 -element proof thus the carrier of TrivOrthoRelStr is 1 -element by CARD_1:49; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; definition func TrivAsymOrthoRelStr -> strict OrthoRelStr equals :: OPOSET_1:def 2 OrthoRelStr(# 1,({} (1,1)),op1 #); coherence OrthoRelStr(# 1,({} (1,1)),op1 #) is strict OrthoRelStr ; end; :: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def_2_:_ TrivAsymOrthoRelStr = OrthoRelStr(# 1,({} (1,1)),op1 #); registration cluster TrivAsymOrthoRelStr -> non empty strict ; coherence not TrivAsymOrthoRelStr is empty ; end; definition let O be non empty OrthoRelStr ; attrO is Dneg means :Def3: :: OPOSET_1:def 3 ex f being Function of O,O st ( f = the Compl of O & f is V252() ); end; :: deftheorem Def3 defines Dneg OPOSET_1:def_3_:_ for O being non empty OrthoRelStr holds ( O is Dneg iff ex f being Function of O,O st ( f = the Compl of O & f is V252() ) ); registration cluster TrivOrthoRelStr -> strict Dneg ; coherence TrivOrthoRelStr is Dneg by Def3; end; registration cluster non empty Dneg for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st b1 is Dneg by Def1; end; definition let O be non empty RelStr ; attrO is SubReFlexive means :Def4: :: OPOSET_1:def 4 the InternalRel of O is reflexive ; end; :: deftheorem Def4 defines SubReFlexive OPOSET_1:def_4_:_ for O being non empty RelStr holds ( O is SubReFlexive iff the InternalRel of O is reflexive ); theorem :: OPOSET_1:2 for O being non empty RelStr st O is reflexive holds O is SubReFlexive proof let O be non empty RelStr ; ::_thesis: ( O is reflexive implies O is SubReFlexive ) assume O is reflexive ; ::_thesis: O is SubReFlexive then the InternalRel of O is_reflexive_in the carrier of O by ORDERS_2:def_2; hence O is SubReFlexive by Def4, PARTIT_2:21; ::_thesis: verum end; theorem Th3: :: OPOSET_1:3 TrivOrthoRelStr is reflexive proof ( rng (id {{}}) = {{}} & field (id {{}}) = (dom (id {{}})) \/ (rng (id {{}})) ) ; hence TrivOrthoRelStr is reflexive by CARD_1:49, ORDERS_2:def_2, RELAT_2:def_9; ::_thesis: verum end; registration cluster TrivOrthoRelStr -> reflexive strict ; coherence TrivOrthoRelStr is reflexive by Th3; end; registration cluster non empty reflexive strict for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is reflexive & b1 is strict ) by Th3; end; definition let O be non empty RelStr ; redefine attr O is irreflexive means :Def5: :: OPOSET_1:def 5 the InternalRel of O is irreflexive ; compatibility ( O is irreflexive iff the InternalRel of O is irreflexive ) proof set RO = the InternalRel of O; A1: field the InternalRel of O c= the carrier of O \/ the carrier of O by RELSET_1:8; thus ( O is irreflexive implies the InternalRel of O is irreflexive ) ::_thesis: ( the InternalRel of O is irreflexive implies O is irreflexive ) proof assume A2: O is irreflexive ; ::_thesis: the InternalRel of O is irreflexive let x be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( not x in field the InternalRel of O or not [x,x] in the InternalRel of O ) thus ( not x in field the InternalRel of O or not [x,x] in the InternalRel of O ) by A1, A2, NECKLACE:def_5; ::_thesis: verum end; assume A3: the InternalRel of O is_irreflexive_in field the InternalRel of O ; :: according to RELAT_2:def_10 ::_thesis: O is irreflexive let x be set ; :: according to NECKLACE:def_5 ::_thesis: ( not x in the carrier of O or not [x,x] in the InternalRel of O ) assume x in the carrier of O ; ::_thesis: not [x,x] in the InternalRel of O percases ( x in field the InternalRel of O or not x in field the InternalRel of O ) ; suppose x in field the InternalRel of O ; ::_thesis: not [x,x] in the InternalRel of O hence not [x,x] in the InternalRel of O by A3, RELAT_2:def_2; ::_thesis: verum end; suppose not x in field the InternalRel of O ; ::_thesis: not [x,x] in the InternalRel of O hence not [x,x] in the InternalRel of O by RELAT_1:15; ::_thesis: verum end; end; end; redefine attr O is irreflexive means :Def6: :: OPOSET_1:def 6 the InternalRel of O is_irreflexive_in the carrier of O; compatibility ( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O ) proof thus ( O is irreflexive implies the InternalRel of O is_irreflexive_in the carrier of O ) ::_thesis: ( the InternalRel of O is_irreflexive_in the carrier of O implies O is irreflexive ) proof assume O is irreflexive ; ::_thesis: the InternalRel of O is_irreflexive_in the carrier of O then for x being set st x in the carrier of O holds not [x,x] in the InternalRel of O by NECKLACE:def_5; hence the InternalRel of O is_irreflexive_in the carrier of O by RELAT_2:def_2; ::_thesis: verum end; assume the InternalRel of O is_irreflexive_in the carrier of O ; ::_thesis: O is irreflexive then for x being set st x in the carrier of O holds not [x,x] in the InternalRel of O by RELAT_2:def_2; hence O is irreflexive by NECKLACE:def_5; ::_thesis: verum end; end; :: deftheorem Def5 defines irreflexive OPOSET_1:def_5_:_ for O being non empty RelStr holds ( O is irreflexive iff the InternalRel of O is irreflexive ); :: deftheorem Def6 defines irreflexive OPOSET_1:def_6_:_ for O being non empty RelStr holds ( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O ); theorem Th4: :: OPOSET_1:4 TrivAsymOrthoRelStr is irreflexive proof for x being set st x in {{}} holds not [x,x] in {} ({{}},{{}}) ; hence TrivAsymOrthoRelStr is irreflexive by Def6, CARD_1:49, RELAT_2:def_2; ::_thesis: verum end; registration cluster TrivAsymOrthoRelStr -> irreflexive strict ; coherence TrivAsymOrthoRelStr is irreflexive by Th4; end; registration cluster non empty irreflexive strict for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is irreflexive & b1 is strict ) by Th4; end; definition let O be non empty RelStr ; redefine attr O is symmetric means :Def7: :: OPOSET_1:def 7 the InternalRel of O is symmetric Relation of the carrier of O; compatibility ( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O ) proof thus ( O is symmetric implies the InternalRel of O is symmetric Relation of the carrier of O ) ::_thesis: ( the InternalRel of O is symmetric Relation of the carrier of O implies O is symmetric ) proof assume the InternalRel of O is_symmetric_in the carrier of O ; :: according to NECKLACE:def_3 ::_thesis: the InternalRel of O is symmetric Relation of the carrier of O hence the InternalRel of O is symmetric Relation of the carrier of O by PARTIT_2:22; ::_thesis: verum end; assume the InternalRel of O is symmetric Relation of the carrier of O ; ::_thesis: O is symmetric hence the InternalRel of O is_symmetric_in the carrier of O by PARTIT_2:23; :: according to NECKLACE:def_3 ::_thesis: verum end; end; :: deftheorem Def7 defines symmetric OPOSET_1:def_7_:_ for O being non empty RelStr holds ( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O ); theorem Th5: :: OPOSET_1:5 TrivOrthoRelStr is symmetric by PARTIT_2:23, NECKLACE:def_3; registration cluster non empty symmetric strict for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is symmetric & b1 is strict ) by Th5; end; definition let O be non empty RelStr ; redefine attr O is antisymmetric means :: OPOSET_1:def 8 the InternalRel of O is antisymmetric Relation of the carrier of O; compatibility ( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O ) proof thus ( O is antisymmetric implies the InternalRel of O is antisymmetric Relation of the carrier of O ) ::_thesis: ( the InternalRel of O is antisymmetric Relation of the carrier of O implies O is antisymmetric ) proof assume the InternalRel of O is_antisymmetric_in the carrier of O ; :: according to ORDERS_2:def_4 ::_thesis: the InternalRel of O is antisymmetric Relation of the carrier of O hence the InternalRel of O is antisymmetric Relation of the carrier of O by PARTIT_2:25; ::_thesis: verum end; assume the InternalRel of O is antisymmetric Relation of the carrier of O ; ::_thesis: O is antisymmetric hence the InternalRel of O is_antisymmetric_in the carrier of O by PARTIT_2:24; :: according to ORDERS_2:def_4 ::_thesis: verum end; end; :: deftheorem defines antisymmetric OPOSET_1:def_8_:_ for O being non empty RelStr holds ( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O ); Lm1: TrivOrthoRelStr is antisymmetric ; registration cluster TrivOrthoRelStr -> symmetric strict ; coherence TrivOrthoRelStr is symmetric by PARTIT_2:23, NECKLACE:def_3; end; registration cluster non empty antisymmetric symmetric strict for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is symmetric & b1 is antisymmetric & b1 is strict ) by Lm1; end; definition let O be non empty RelStr ; redefine attr O is asymmetric means :Def9: :: OPOSET_1:def 9 the InternalRel of O is_asymmetric_in the carrier of O; compatibility ( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O ) proof thus ( O is asymmetric implies the InternalRel of O is_asymmetric_in the carrier of O ) ::_thesis: ( the InternalRel of O is_asymmetric_in the carrier of O implies O is asymmetric ) proof assume the InternalRel of O is asymmetric ; :: according to NECKLACE:def_4 ::_thesis: the InternalRel of O is_asymmetric_in the carrier of O hence the InternalRel of O is_asymmetric_in the carrier of O by PARTIT_2:28; ::_thesis: verum end; assume the InternalRel of O is_asymmetric_in the carrier of O ; ::_thesis: O is asymmetric hence the InternalRel of O is asymmetric by PARTIT_2:29; :: according to NECKLACE:def_4 ::_thesis: verum end; end; :: deftheorem Def9 defines asymmetric OPOSET_1:def_9_:_ for O being non empty RelStr holds ( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O ); theorem Th6: :: OPOSET_1:6 TrivAsymOrthoRelStr is asymmetric by PARTIT_2:28, Def9; registration cluster TrivAsymOrthoRelStr -> asymmetric strict ; coherence TrivAsymOrthoRelStr is asymmetric by PARTIT_2:28, Def9; end; registration cluster non empty asymmetric strict for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is asymmetric & b1 is strict ) by Th6; end; definition let O be non empty RelStr ; redefine attr O is transitive means :Def10: :: OPOSET_1:def 10 the InternalRel of O is transitive Relation of the carrier of O; compatibility ( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O ) proof thus ( O is transitive implies the InternalRel of O is transitive Relation of the carrier of O ) ::_thesis: ( the InternalRel of O is transitive Relation of the carrier of O implies O is transitive ) proof assume the InternalRel of O is_transitive_in the carrier of O ; :: according to ORDERS_2:def_3 ::_thesis: the InternalRel of O is transitive Relation of the carrier of O hence the InternalRel of O is transitive Relation of the carrier of O by PARTIT_2:27; ::_thesis: verum end; assume the InternalRel of O is transitive Relation of the carrier of O ; ::_thesis: O is transitive hence the InternalRel of O is_transitive_in the carrier of O by PARTIT_2:26; :: according to ORDERS_2:def_3 ::_thesis: verum end; end; :: deftheorem Def10 defines transitive OPOSET_1:def_10_:_ for O being non empty RelStr holds ( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O ); registration cluster non empty reflexive transitive antisymmetric symmetric strict for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is reflexive & b1 is symmetric & b1 is antisymmetric & b1 is transitive & b1 is strict ) by Lm1; end; theorem :: OPOSET_1:7 TrivAsymOrthoRelStr is transitive by PARTIT_2:26, ORDERS_2:def_3; registration cluster TrivAsymOrthoRelStr -> transitive asymmetric irreflexive strict ; coherence ( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is asymmetric & TrivAsymOrthoRelStr is transitive ) by PARTIT_2:26, ORDERS_2:def_3; end; registration cluster non empty transitive asymmetric irreflexive strict for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is irreflexive & b1 is asymmetric & b1 is transitive & b1 is strict ) by Th4; end; theorem :: OPOSET_1:8 for O being non empty RelStr st O is symmetric & O is transitive holds O is SubReFlexive proof let O be non empty RelStr ; ::_thesis: ( O is symmetric & O is transitive implies O is SubReFlexive ) set R = the InternalRel of O; assume ( O is symmetric & O is transitive ) ; ::_thesis: O is SubReFlexive then ( the InternalRel of O is symmetric & the InternalRel of O is transitive ) by Def7, Def10; hence O is SubReFlexive by Def4; ::_thesis: verum end; theorem :: OPOSET_1:9 for O being non empty RelStr st O is irreflexive & O is transitive holds O is asymmetric proof let O be non empty RelStr ; ::_thesis: ( O is irreflexive & O is transitive implies O is asymmetric ) set R = the InternalRel of O; assume ( O is irreflexive & O is transitive ) ; ::_thesis: O is asymmetric then ( the InternalRel of O is irreflexive & the InternalRel of O is transitive ) by Def5, Def10; hence O is asymmetric by NECKLACE:def_4; ::_thesis: verum end; theorem Th10: :: OPOSET_1:10 for O being non empty RelStr st O is asymmetric holds O is irreflexive proof let O be non empty RelStr ; ::_thesis: ( O is asymmetric implies O is irreflexive ) set R = the InternalRel of O; assume O is asymmetric ; ::_thesis: O is irreflexive then the InternalRel of O is asymmetric by NECKLACE:def_4; hence O is irreflexive by Def5; ::_thesis: verum end; begin definition let O be non empty RelStr ; attrO is SubQuasiOrdered means :Def11: :: OPOSET_1:def 11 ( O is SubReFlexive & O is transitive ); end; :: deftheorem Def11 defines SubQuasiOrdered OPOSET_1:def_11_:_ for O being non empty RelStr holds ( O is SubQuasiOrdered iff ( O is SubReFlexive & O is transitive ) ); notation let O be non empty RelStr ; synonym SubPreOrdered O for SubQuasiOrdered ; end; definition let O be non empty RelStr ; attrO is QuasiOrdered means :Def12: :: OPOSET_1:def 12 ( O is reflexive & O is transitive ); end; :: deftheorem Def12 defines QuasiOrdered OPOSET_1:def_12_:_ for O being non empty RelStr holds ( O is QuasiOrdered iff ( O is reflexive & O is transitive ) ); notation let O be non empty RelStr ; synonym PreOrdered O for QuasiOrdered ; end; theorem Th11: :: OPOSET_1:11 for O being non empty RelStr st O is QuasiOrdered holds O is SubQuasiOrdered proof let O be non empty RelStr ; ::_thesis: ( O is QuasiOrdered implies O is SubQuasiOrdered ) set IntRel = the InternalRel of O; set CO = the carrier of O; assume A1: O is QuasiOrdered ; ::_thesis: O is SubQuasiOrdered then A2: O is transitive by Def12; O is reflexive by A1, Def12; then the InternalRel of O is_reflexive_in the carrier of O by ORDERS_2:def_2; then the InternalRel of O is reflexive by PARTIT_2:21; hence O is SubQuasiOrdered by A2, Def11, Def4; ::_thesis: verum end; registration cluster non empty QuasiOrdered -> non empty SubQuasiOrdered for OrthoRelStr ; correctness coherence for b1 being non empty OrthoRelStr st b1 is QuasiOrdered holds b1 is SubQuasiOrdered ; by Th11; end; registration cluster TrivOrthoRelStr -> strict QuasiOrdered ; coherence TrivOrthoRelStr is QuasiOrdered by Def12; end; definition let O be non empty OrthoRelStr ; attrO is QuasiPure means :Def13: :: OPOSET_1:def 13 ( O is Dneg & O is QuasiOrdered ); end; :: deftheorem Def13 defines QuasiPure OPOSET_1:def_13_:_ for O being non empty OrthoRelStr holds ( O is QuasiPure iff ( O is Dneg & O is QuasiOrdered ) ); registration cluster non empty strict Dneg QuasiOrdered QuasiPure for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is QuasiPure & b1 is Dneg & b1 is QuasiOrdered & b1 is strict ) proof TrivOrthoRelStr is QuasiPure by Def13; hence ex b1 being non empty OrthoRelStr st ( b1 is QuasiPure & b1 is Dneg & b1 is QuasiOrdered & b1 is strict ) ; ::_thesis: verum end; end; registration cluster TrivOrthoRelStr -> strict QuasiPure ; coherence TrivOrthoRelStr is QuasiPure by Def13; end; definition mode QuasiPureOrthoRelStr is non empty QuasiPure OrthoRelStr ; end; definition let O be non empty OrthoRelStr ; attrO is PartialOrdered means :Def14: :: OPOSET_1:def 14 ( O is reflexive & O is antisymmetric & O is transitive ); end; :: deftheorem Def14 defines PartialOrdered OPOSET_1:def_14_:_ for O being non empty OrthoRelStr holds ( O is PartialOrdered iff ( O is reflexive & O is antisymmetric & O is transitive ) ); registration cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric for OrthoRelStr ; coherence for b1 being non empty OrthoRelStr st b1 is PartialOrdered holds ( b1 is reflexive & b1 is antisymmetric & b1 is transitive ) by Def14; cluster non empty reflexive transitive antisymmetric -> non empty PartialOrdered for OrthoRelStr ; coherence for b1 being non empty OrthoRelStr st b1 is reflexive & b1 is antisymmetric & b1 is transitive holds b1 is PartialOrdered by Def14; end; definition let O be non empty OrthoRelStr ; attrO is Pure means :Def15: :: OPOSET_1:def 15 ( O is Dneg & O is PartialOrdered ); end; :: deftheorem Def15 defines Pure OPOSET_1:def_15_:_ for O being non empty OrthoRelStr holds ( O is Pure iff ( O is Dneg & O is PartialOrdered ) ); registration cluster non empty strict Dneg PartialOrdered Pure for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is Pure & b1 is Dneg & b1 is PartialOrdered & b1 is strict ) proof TrivOrthoRelStr is Pure by Def15; hence ex b1 being non empty OrthoRelStr st ( b1 is Pure & b1 is Dneg & b1 is PartialOrdered & b1 is strict ) ; ::_thesis: verum end; end; registration cluster TrivOrthoRelStr -> strict Pure ; coherence TrivOrthoRelStr is Pure by Def15; end; definition mode PureOrthoRelStr is non empty Pure OrthoRelStr ; end; definition let O be non empty OrthoRelStr ; attrO is StrictPartialOrdered means :Def16: :: OPOSET_1:def 16 ( O is asymmetric & O is transitive ); end; :: deftheorem Def16 defines StrictPartialOrdered OPOSET_1:def_16_:_ for O being non empty OrthoRelStr holds ( O is StrictPartialOrdered iff ( O is asymmetric & O is transitive ) ); notation let O be non empty OrthoRelStr ; synonym StrictOrdered O for StrictPartialOrdered ; end; theorem Th12: :: OPOSET_1:12 for O being non empty OrthoRelStr st O is StrictPartialOrdered holds O is irreflexive proof let O be non empty OrthoRelStr ; ::_thesis: ( O is StrictPartialOrdered implies O is irreflexive ) assume O is StrictPartialOrdered ; ::_thesis: O is irreflexive then ( O is asymmetric & O is transitive ) by Def16; hence O is irreflexive by Th10; ::_thesis: verum end; registration cluster non empty StrictPartialOrdered -> non empty irreflexive for OrthoRelStr ; coherence for b1 being non empty OrthoRelStr st b1 is StrictPartialOrdered holds b1 is irreflexive by Th12; end; registration cluster non empty StrictPartialOrdered -> non empty irreflexive for OrthoRelStr ; coherence for b1 being non empty OrthoRelStr st b1 is StrictPartialOrdered holds b1 is irreflexive ; end; registration cluster TrivAsymOrthoRelStr -> irreflexive strict StrictPartialOrdered ; coherence ( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is StrictPartialOrdered ) by Def16; end; registration cluster non empty irreflexive strict StrictPartialOrdered for OrthoRelStr ; existence ex b1 being non empty strict OrthoRelStr st ( b1 is irreflexive & b1 is StrictPartialOrdered ) proof TrivAsymOrthoRelStr is StrictPartialOrdered ; hence ex b1 being non empty strict OrthoRelStr st ( b1 is irreflexive & b1 is StrictPartialOrdered ) ; ::_thesis: verum end; end; theorem :: OPOSET_1:13 for QO being non empty QuasiOrdered OrthoRelStr st QO is antisymmetric holds QO is PartialOrdered proof let QO be non empty QuasiOrdered OrthoRelStr ; ::_thesis: ( QO is antisymmetric implies QO is PartialOrdered ) assume A1: QO is antisymmetric ; ::_thesis: QO is PartialOrdered ( QO is reflexive & QO is transitive ) by Def12; hence QO is PartialOrdered by A1; ::_thesis: verum end; registration cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric for OrthoRelStr ; correctness coherence for b1 being non empty OrthoRelStr st b1 is PartialOrdered holds ( b1 is reflexive & b1 is transitive & b1 is antisymmetric ); ; end; definition let PO be non empty RelStr ; let f be UnOp of the carrier of PO; attrf is Orderinvolutive means :Def17: :: OPOSET_1:def 17 ( f is V252() & f is antitone ); end; :: deftheorem Def17 defines Orderinvolutive OPOSET_1:def_17_:_ for PO being non empty RelStr for f being UnOp of the carrier of PO holds ( f is Orderinvolutive iff ( f is V252() & f is antitone ) ); definition let PO be non empty OrthoRelStr ; attrPO is OrderInvolutive means :Def18: :: OPOSET_1:def 18 the Compl of PO is Orderinvolutive ; end; :: deftheorem Def18 defines OrderInvolutive OPOSET_1:def_18_:_ for PO being non empty OrthoRelStr holds ( PO is OrderInvolutive iff the Compl of PO is Orderinvolutive ); theorem Th14: :: OPOSET_1:14 the Compl of TrivOrthoRelStr is Orderinvolutive proof set O = TrivOrthoRelStr ; set C = the Compl of TrivOrthoRelStr; reconsider Emp = {} as Element of TrivOrthoRelStr by CARD_1:49, TARSKI:def_1; the Compl of TrivOrthoRelStr is antitone Function of TrivOrthoRelStr,TrivOrthoRelStr proof reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr,TrivOrthoRelStr ; for x1, x2 being Element of TrivOrthoRelStr st x1 <= x2 holds for y1, y2 being Element of TrivOrthoRelStr st y1 = f . x1 & y2 = f . x2 holds y1 >= y2 proof let a1, a2 be Element of TrivOrthoRelStr; ::_thesis: ( a1 <= a2 implies for y1, y2 being Element of TrivOrthoRelStr st y1 = f . a1 & y2 = f . a2 holds y1 >= y2 ) set b1 = f . a1; f . a1 = Emp by CARD_1:49, FUNCT_2:50; then f . a2 <= f . a1 by CARD_1:49, FUNCT_2:50; hence ( a1 <= a2 implies for y1, y2 being Element of TrivOrthoRelStr st y1 = f . a1 & y2 = f . a2 holds y1 >= y2 ) ; ::_thesis: verum end; hence the Compl of TrivOrthoRelStr is antitone Function of TrivOrthoRelStr,TrivOrthoRelStr by WAYBEL_0:def_5; ::_thesis: verum end; hence the Compl of TrivOrthoRelStr is Orderinvolutive by Def17; ::_thesis: verum end; registration cluster TrivOrthoRelStr -> strict OrderInvolutive ; coherence TrivOrthoRelStr is OrderInvolutive by Def18, Th14; end; registration cluster non empty PartialOrdered Pure OrderInvolutive for OrthoRelStr ; existence ex b1 being non empty OrthoRelStr st ( b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered ) proof take TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is OrderInvolutive & TrivOrthoRelStr is Pure & TrivOrthoRelStr is PartialOrdered ) thus ( TrivOrthoRelStr is OrderInvolutive & TrivOrthoRelStr is Pure & TrivOrthoRelStr is PartialOrdered ) ; ::_thesis: verum end; end; definition mode PreOrthoPoset is non empty PartialOrdered Pure OrderInvolutive OrthoRelStr ; end; definition let PO be non empty RelStr ; let f be UnOp of the carrier of PO; predf QuasiOrthoComplement_on PO means :Def19: :: OPOSET_1:def 19 ( f is Orderinvolutive & ( for y being Element of PO holds ( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO ) ) ); end; :: deftheorem Def19 defines QuasiOrthoComplement_on OPOSET_1:def_19_:_ for PO being non empty RelStr for f being UnOp of the carrier of PO holds ( f QuasiOrthoComplement_on PO iff ( f is Orderinvolutive & ( for y being Element of PO holds ( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO ) ) ) ); definition let PO be non empty OrthoRelStr ; attrPO is QuasiOrthocomplemented means :Def20: :: OPOSET_1:def 20 ex f being Function of PO,PO st ( f = the Compl of PO & f QuasiOrthoComplement_on PO ); end; :: deftheorem Def20 defines QuasiOrthocomplemented OPOSET_1:def_20_:_ for PO being non empty OrthoRelStr holds ( PO is QuasiOrthocomplemented iff ex f being Function of PO,PO st ( f = the Compl of PO & f QuasiOrthoComplement_on PO ) ); Lm2: id {{}} = {[{},{}]} by SYSREL:13; theorem Th15: :: OPOSET_1:15 TrivOrthoRelStr is QuasiOrthocomplemented proof set O = TrivOrthoRelStr ; set C = the Compl of TrivOrthoRelStr; set S = the carrier of TrivOrthoRelStr; the Compl of TrivOrthoRelStr QuasiOrthoComplement_on TrivOrthoRelStr proof reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr,TrivOrthoRelStr ; A1: for x being Element of the carrier of TrivOrthoRelStr holds {x,(op1 . x)} = {x} proof let a be Element of the carrier of TrivOrthoRelStr; ::_thesis: {a,(op1 . a)} = {a} a = op1 . a by Lm2, CARD_1:49, FUNCT_1:17, PARTIT_2:19; hence {a,(op1 . a)} = {a} by ENUMSET1:29; ::_thesis: verum end; for x being Element of TrivOrthoRelStr holds ( sup {x,(f . x)} = x & inf {x,(f . x)} = x & ex_sup_of {x,(f . x)}, TrivOrthoRelStr & ex_inf_of {x,(f . x)}, TrivOrthoRelStr ) proof let a be Element of TrivOrthoRelStr; ::_thesis: ( sup {a,(f . a)} = a & inf {a,(f . a)} = a & ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr ) {a,(f . a)} = {a} by A1; hence ( sup {a,(f . a)} = a & inf {a,(f . a)} = a & ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr ) by YELLOW_0:38, YELLOW_0:39; ::_thesis: verum end; hence the Compl of TrivOrthoRelStr QuasiOrthoComplement_on TrivOrthoRelStr by Def19, Th14; ::_thesis: verum end; hence TrivOrthoRelStr is QuasiOrthocomplemented by Def20; ::_thesis: verum end; definition let PO be non empty RelStr ; let f be UnOp of the carrier of PO; predf OrthoComplement_on PO means :Def21: :: OPOSET_1:def 21 ( f is Orderinvolutive & ( for y being Element of PO holds ( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO & "\/" ({y,(f . y)},PO) is_maximum_of the carrier of PO & "/\" ({y,(f . y)},PO) is_minimum_of the carrier of PO ) ) ); end; :: deftheorem Def21 defines OrthoComplement_on OPOSET_1:def_21_:_ for PO being non empty RelStr for f being UnOp of the carrier of PO holds ( f OrthoComplement_on PO iff ( f is Orderinvolutive & ( for y being Element of PO holds ( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO & "\/" ({y,(f . y)},PO) is_maximum_of the carrier of PO & "/\" ({y,(f . y)},PO) is_minimum_of the carrier of PO ) ) ) ); definition let PO be non empty OrthoRelStr ; attrPO is Orthocomplemented means :Def22: :: OPOSET_1:def 22 ex f being Function of PO,PO st ( f = the Compl of PO & f OrthoComplement_on PO ); end; :: deftheorem Def22 defines Orthocomplemented OPOSET_1:def_22_:_ for PO being non empty OrthoRelStr holds ( PO is Orthocomplemented iff ex f being Function of PO,PO st ( f = the Compl of PO & f OrthoComplement_on PO ) ); theorem :: OPOSET_1:16 for PO being non empty OrthoRelStr for f being UnOp of the carrier of PO st f OrthoComplement_on PO holds f QuasiOrthoComplement_on PO proof let PO be non empty OrthoRelStr ; ::_thesis: for f being UnOp of the carrier of PO st f OrthoComplement_on PO holds f QuasiOrthoComplement_on PO let g be UnOp of the carrier of PO; ::_thesis: ( g OrthoComplement_on PO implies g QuasiOrthoComplement_on PO ) assume g OrthoComplement_on PO ; ::_thesis: g QuasiOrthoComplement_on PO then ( ( for x being Element of PO holds ( ex_sup_of {x,(g . x)},PO & ex_inf_of {x,(g . x)},PO ) ) & g is Orderinvolutive ) by Def21; hence g QuasiOrthoComplement_on PO by Def19; ::_thesis: verum end; theorem Th17: :: OPOSET_1:17 TrivOrthoRelStr is Orthocomplemented proof set O = TrivOrthoRelStr ; set C = the Compl of TrivOrthoRelStr; set S = the carrier of TrivOrthoRelStr; reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr,TrivOrthoRelStr ; f OrthoComplement_on TrivOrthoRelStr proof reconsider f = the Compl of TrivOrthoRelStr as Function of TrivOrthoRelStr,TrivOrthoRelStr ; A1: for x being Element of the carrier of TrivOrthoRelStr holds {x,(op1 . x)} = {x} proof let a be Element of the carrier of TrivOrthoRelStr; ::_thesis: {a,(op1 . a)} = {a} a = op1 . a by Lm2, CARD_1:49, FUNCT_1:17, PARTIT_2:19; hence {a,(op1 . a)} = {a} by ENUMSET1:29; ::_thesis: verum end; A2: for x being Element of TrivOrthoRelStr holds ( ex_sup_of {x,(f . x)}, TrivOrthoRelStr & ex_inf_of {x,(f . x)}, TrivOrthoRelStr & sup {x,(f . x)} = x & inf {x,(f . x)} = x ) proof let a be Element of TrivOrthoRelStr; ::_thesis: ( ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr & sup {a,(f . a)} = a & inf {a,(f . a)} = a ) {a,(f . a)} = {a} by A1; hence ( ex_sup_of {a,(f . a)}, TrivOrthoRelStr & ex_inf_of {a,(f . a)}, TrivOrthoRelStr & sup {a,(f . a)} = a & inf {a,(f . a)} = a ) by YELLOW_0:38, YELLOW_0:39; ::_thesis: verum end; A3: for x being Element of TrivOrthoRelStr holds ( sup {x,(f . x)} in {x,(f . x)} & inf {x,(f . x)} in {x,(f . x)} ) proof let a be Element of TrivOrthoRelStr; ::_thesis: ( sup {a,(f . a)} in {a,(f . a)} & inf {a,(f . a)} in {a,(f . a)} ) ( sup {a,(f . a)} = a & inf {a,(f . a)} = a ) by A2; hence ( sup {a,(f . a)} in {a,(f . a)} & inf {a,(f . a)} in {a,(f . a)} ) by TARSKI:def_2; ::_thesis: verum end; A4: for x being Element of TrivOrthoRelStr holds ( x is_maximum_of {x,(f . x)} & x is_minimum_of {x,(f . x)} ) proof let a be Element of TrivOrthoRelStr; ::_thesis: ( a is_maximum_of {a,(f . a)} & a is_minimum_of {a,(f . a)} ) A5: ( sup {a,(f . a)} = a & ex_sup_of {a,(f . a)}, TrivOrthoRelStr ) by A2; ( sup {a,(f . a)} in {a,(f . a)} & inf {a,(f . a)} = a ) by A2, A3; hence ( a is_maximum_of {a,(f . a)} & a is_minimum_of {a,(f . a)} ) by A5, A2, WAYBEL_1:def_6, WAYBEL_1:def_7; ::_thesis: verum end; for y being Element of TrivOrthoRelStr holds ( sup {y,(f . y)} is_maximum_of the carrier of TrivOrthoRelStr & inf {y,(f . y)} is_minimum_of the carrier of TrivOrthoRelStr ) proof let a be Element of TrivOrthoRelStr; ::_thesis: ( sup {a,(f . a)} is_maximum_of the carrier of TrivOrthoRelStr & inf {a,(f . a)} is_minimum_of the carrier of TrivOrthoRelStr ) reconsider a0 = a as Element of the carrier of TrivOrthoRelStr ; {a0,(f . a0)} = {a0} by A1; then A7: {a0,(f . a0)} = the carrier of TrivOrthoRelStr by CARD_1:49, TARSKI:def_1; ( a is_maximum_of {a,(f . a)} & a is_minimum_of {a,(f . a)} ) by A4; hence ( sup {a,(f . a)} is_maximum_of the carrier of TrivOrthoRelStr & inf {a,(f . a)} is_minimum_of the carrier of TrivOrthoRelStr ) by A2, A7; ::_thesis: verum end; hence f OrthoComplement_on TrivOrthoRelStr by A2, Def21, Th14; ::_thesis: verum end; hence TrivOrthoRelStr is Orthocomplemented by Def22; ::_thesis: verum end; registration cluster TrivOrthoRelStr -> strict QuasiOrthocomplemented Orthocomplemented ; coherence ( TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is Orthocomplemented ) by Th15, Th17; end; registration cluster non empty PartialOrdered QuasiOrthocomplemented Orthocomplemented for OrthoRelStr ; correctness existence ex b1 being non empty OrthoRelStr st ( b1 is Orthocomplemented & b1 is QuasiOrthocomplemented & b1 is PartialOrdered ); proof take TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is Orthocomplemented & TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is PartialOrdered ) thus ( TrivOrthoRelStr is Orthocomplemented & TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is PartialOrdered ) ; ::_thesis: verum end; end; definition mode QuasiOrthoPoset is non empty PartialOrdered QuasiOrthocomplemented OrthoRelStr ; mode OrthoPoset is non empty PartialOrdered Orthocomplemented OrthoRelStr ; end;