:: 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;