:: Basic Notions and Properties of Orthoposets
:: by Markus Moschner
::
:: Received February 11, 2003
:: Copyright (c) 2003 Association of Mizar Users

notation

let A, B be set ;
synonym [#] A,B for [:A,B:];

end;

definition

let A, B be set ;
func {} A,B -> Relation of A,B equals :: OPOSET_1:def 1
{} ;
correctness
coherence
{} is Relation of A,B;
by RELSET_1:25;
:: original: [#]
redefine func [#] A,B -> Relation of A,B;
correctness
coherence
[#] A,B is Relation of A,B;

proof end;

canceled;

end;

:: deftheorem defines {} OPOSET_1:def 1 :

for A, B being set holds {} A,B = {} ;

:: deftheorem OPOSET_1:def 2 :

canceled;

theorem Th1: :: OPOSET_1:1

for X being non empty set holds field (id X) = X

proof end;

Lm1: id {{} } = {[{} ,{} ]}
by SYSREL:30;

theorem :: OPOSET_1:2

canceled;

theorem Th3: :: OPOSET_1:3

op1 = {[{} ,{} ]}

proof end;

theorem :: OPOSET_1:4

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

theorem :: OPOSET_1:5

canceled;

theorem Th6: :: OPOSET_1:6

for A, B being set holds field ({} A,B) = {}

proof end;

theorem Th7: :: OPOSET_1:7

for X being non empty set
for R being Relation of X st R is_reflexive_in X holds
( R is reflexive & field R = X )

proof end;

theorem Th8: :: OPOSET_1:8

for X being non empty set
for R being Relation of X st R is_symmetric_in X holds
R is symmetric

proof end;

theorem Th9: :: OPOSET_1:9

for X, S being non empty set
for R being Relation of X st R is symmetric & field R c= S holds
R is_symmetric_in S

proof end;

theorem Th10: :: OPOSET_1:10

for X, S being non empty set
for R being Relation of X st R is antisymmetric & field R c= S holds
R is_antisymmetric_in S

proof end;

theorem Th11: :: OPOSET_1:11

for X being non empty set
for R being Relation of X st R is_antisymmetric_in X holds
R is antisymmetric

proof end;

theorem Th12: :: OPOSET_1:12

for X, S being non empty set
for R being Relation of X st R is transitive & field R c= S holds
R is_transitive_in S

proof end;

theorem Th13: :: OPOSET_1:13

for X being non empty set
for R being Relation of X st R is_transitive_in X holds
R is transitive

proof end;

theorem Th14: :: OPOSET_1:14

for X, S being non empty set
for R being Relation of X st R is asymmetric & field R c= S holds
R is_asymmetric_in S

proof end;

theorem Th15: :: OPOSET_1:15

for X being non empty set
for R being Relation of X st R is_asymmetric_in X holds
R is asymmetric

proof end;

theorem Th16: :: OPOSET_1:16

for X, S being non empty set
for R being Relation of X st R is irreflexive & field R c= S holds
R is_irreflexive_in S

proof end;

theorem Th17: :: OPOSET_1:17

for X being non empty set
for R being Relation of X st R is_irreflexive_in X holds
R is irreflexive

proof end;

registration

let X be set ;
cluster irreflexive asymmetric transitive Element of bool ([#] X,X);
existence
ex b₁ being Relation of X st
( b₁ is irreflexive & b₁ is asymmetric & b₁ is transitive )

proof 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 OrthoRelStr ;
existence
ex b₁ being OrthoRelStr st
( not b₁ is empty & b₁ is strict )

proof end;

end;

definition

let X be non empty set ;
let f be Function of X,X;
attr f is dneg means :Def3: :: OPOSET_1:def 3
for x being Element of X holds f . (f . x) = x;

end;

:: deftheorem Def3 defines dneg OPOSET_1:def 3 :

for X being non empty set
for f being Function of X,X holds
( f is dneg iff for x being Element of X holds f . (f . x) = x );

notation

let X be non empty set ;
let f be Function of X,X;
synonym involutive f for dneg ;

end;

theorem :: OPOSET_1:18

canceled;

theorem Th19: :: OPOSET_1:19

op1 is dneg

proof end;

theorem Th20: :: OPOSET_1:20

for X being non empty set holds id X is dneg

proof end;

registration

let O be non empty OrthoRelStr ;
cluster dneg Element of bool ([#] the carrier of O,the carrier of O);
existence
ex b₁ being Function of O,O st b₁ is dneg

proof end;

end;

definition

func TrivOrthoRelStr -> strict OrthoRelStr equals :Def4: :: OPOSET_1:def 4
OrthoRelStr(# 1,(id 1),op1 #);
coherence
OrthoRelStr(# 1,(id 1),op1 #) is strict OrthoRelStr ;

end;

:: deftheorem Def4 defines TrivOrthoRelStr OPOSET_1:def 4 :

TrivOrthoRelStr = OrthoRelStr(# 1,(id 1),op1 #);

notation

synonym TrivPoset for TrivOrthoRelStr ;

end;

registration

cluster TrivOrthoRelStr -> non empty trivial strict ;
coherence
( not TrivOrthoRelStr is empty & TrivOrthoRelStr is trivial ) by CARD_1:87, REALSET1:def 4;

end;

definition

func TrivAsymOrthoRelStr -> strict OrthoRelStr equals :: OPOSET_1:def 5
OrthoRelStr(# 1,({} 1,1),op1 #);
coherence
OrthoRelStr(# 1,({} 1,1),op1 #) is strict OrthoRelStr ;

end;

:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 5 :

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 ;
attr O is Dneg means :Def6: :: OPOSET_1:def 6
ex f being Function of O,O st
( f = the Compl of O & f is dneg );

end;

:: deftheorem Def6 defines Dneg OPOSET_1:def 6 :

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 dneg ) );

theorem :: OPOSET_1:21

TrivOrthoRelStr is Dneg by Def6, Th19;

registration

cluster TrivOrthoRelStr -> strict Dneg ;
coherence
TrivOrthoRelStr is Dneg by Def6, Th19;

end;

registration

cluster non empty Dneg OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st b₁ is Dneg by Def4;

end;

definition

let O be non empty RelStr ;
canceled;
canceled;
attr O is SubReFlexive means :Def9: :: OPOSET_1:def 9
the InternalRel of O is reflexive ;

end;

:: deftheorem OPOSET_1:def 7 :

canceled;

:: deftheorem OPOSET_1:def 8 :

canceled;

:: deftheorem Def9 defines SubReFlexive OPOSET_1:def 9 :

for O being non empty RelStr holds
( O is SubReFlexive iff the InternalRel of O is reflexive );

theorem :: OPOSET_1:22

for O being non empty RelStr st O is reflexive holds
O is SubReFlexive

proof end;

theorem Th23: :: OPOSET_1:23

TrivOrthoRelStr is reflexive

proof end;

registration

cluster TrivOrthoRelStr -> reflexive strict ;
coherence
TrivOrthoRelStr is reflexive by Th23;

end;

registration

cluster non empty reflexive strict OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is reflexive & b₁ is strict ) by Th23;

end;

definition

let O be non empty RelStr ;
canceled;
attr O is SubIrreFlexive means :Def11: :: OPOSET_1:def 11
the InternalRel of O is irreflexive ;
redefine attr O is irreflexive means :Def12: :: OPOSET_1:def 12
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 end;

end;

:: deftheorem OPOSET_1:def 10 :

canceled;

:: deftheorem Def11 defines SubIrreFlexive OPOSET_1:def 11 :

for O being non empty RelStr holds
( O is SubIrreFlexive iff the InternalRel of O is irreflexive );

:: deftheorem Def12 defines irreflexive OPOSET_1:def 12 :

for O being non empty RelStr holds
( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O );

theorem Th24: :: OPOSET_1:24

for O being non empty RelStr st O is irreflexive holds
O is SubIrreFlexive

proof end;

theorem Th25: :: OPOSET_1:25

TrivAsymOrthoRelStr is irreflexive

proof end;

registration

cluster non empty irreflexive -> non empty SubIrreFlexive OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is irreflexive holds
b₁ is SubIrreFlexive ;
by Th24;

end;

registration

cluster TrivAsymOrthoRelStr -> irreflexive strict ;
coherence
TrivAsymOrthoRelStr is irreflexive by Th25;

end;

registration

cluster non empty irreflexive strict OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is irreflexive & b₁ is strict ) by Th25;

end;

definition

let O be non empty RelStr ;
attr O is SubSymmetric means :Def13: :: OPOSET_1:def 13
the InternalRel of O is symmetric Relation of the carrier of O;

end;

:: deftheorem Def13 defines SubSymmetric OPOSET_1:def 13 :

for O being non empty RelStr holds
( O is SubSymmetric iff the InternalRel of O is symmetric Relation of the carrier of O );

theorem Th26: :: OPOSET_1:26

for O being non empty RelStr st O is symmetric holds
O is SubSymmetric

proof end;

theorem Th27: :: OPOSET_1:27

TrivOrthoRelStr is symmetric

proof end;

registration

cluster non empty symmetric -> non empty SubSymmetric OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is symmetric holds
b₁ is SubSymmetric ;
by Th26;

end;

registration

cluster non empty symmetric strict OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is symmetric & b₁ is strict ) by Th27;

end;

definition

let O be non empty RelStr ;
canceled;
attr O is SubAntisymmetric means :Def15: :: OPOSET_1:def 15
the InternalRel of O is antisymmetric Relation of the carrier of O;

end;

:: deftheorem OPOSET_1:def 14 :

canceled;

:: deftheorem Def15 defines SubAntisymmetric OPOSET_1:def 15 :

for O being non empty RelStr holds
( O is SubAntisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O );

theorem Th28: :: OPOSET_1:28

for O being non empty RelStr st O is antisymmetric holds
O is SubAntisymmetric

proof end;

Lm3: TrivOrthoRelStr is antisymmetric
;

registration

cluster non empty antisymmetric -> non empty SubAntisymmetric OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is antisymmetric holds
b₁ is SubAntisymmetric ;
by Th28;

end;

registration

cluster TrivOrthoRelStr -> symmetric strict ;
coherence
TrivOrthoRelStr is symmetric by Th27;

end;

registration

cluster non empty antisymmetric symmetric strict OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is symmetric & b₁ is antisymmetric & b₁ is strict ) by Lm3;

end;

definition

let O be non empty RelStr ;
canceled;
canceled;
attr O is Asymmetric means :Def18: :: OPOSET_1:def 18
the InternalRel of O is_asymmetric_in the carrier of O;

end;

:: deftheorem OPOSET_1:def 16 :

canceled;

:: deftheorem OPOSET_1:def 17 :

canceled;

:: deftheorem Def18 defines Asymmetric OPOSET_1:def 18 :

for O being non empty RelStr holds
( O is Asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O );

theorem :: OPOSET_1:29

canceled;

theorem Th30: :: OPOSET_1:30

for O being non empty RelStr st O is Asymmetric holds
O is asymmetric

proof end;

theorem Th31: :: OPOSET_1:31

TrivAsymOrthoRelStr is Asymmetric

proof end;

registration

cluster non empty Asymmetric -> non empty asymmetric OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is Asymmetric holds
b₁ is asymmetric ;
by Th30;

end;

registration

cluster TrivAsymOrthoRelStr -> strict Asymmetric ;
coherence
TrivAsymOrthoRelStr is Asymmetric by Th31;

end;

registration

cluster non empty strict Asymmetric OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is Asymmetric & b₁ is strict ) by Th31;

end;

definition

let O be non empty RelStr ;
attr O is SubTransitive means :Def19: :: OPOSET_1:def 19
the InternalRel of O is transitive Relation of the carrier of O;

end;

:: deftheorem Def19 defines SubTransitive OPOSET_1:def 19 :

for O being non empty RelStr holds
( O is SubTransitive iff the InternalRel of O is transitive Relation of the carrier of O );

theorem Th32: :: OPOSET_1:32

for O being non empty RelStr st O is transitive holds
O is SubTransitive

proof end;

registration

cluster non empty transitive -> non empty SubTransitive OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is transitive holds
b₁ is SubTransitive ;
by Th32;

end;

registration

cluster non empty reflexive transitive antisymmetric symmetric strict OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is reflexive & b₁ is symmetric & b₁ is antisymmetric & b₁ is transitive & b₁ is strict ) by Lm3;

end;

theorem :: OPOSET_1:33

canceled;

theorem Th34: :: OPOSET_1:34

TrivAsymOrthoRelStr is transitive

proof end;

registration

cluster TrivAsymOrthoRelStr -> transitive irreflexive strict Asymmetric ;
coherence
( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is Asymmetric & TrivAsymOrthoRelStr is transitive ) by Th34;

end;

registration

cluster non empty transitive irreflexive strict Asymmetric OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is irreflexive & b₁ is Asymmetric & b₁ is transitive & b₁ is strict ) by Th25;

end;

theorem :: OPOSET_1:35

for O being non empty RelStr st O is SubSymmetric & O is SubTransitive holds
O is SubReFlexive

proof end;

theorem :: OPOSET_1:36

for O being non empty RelStr st O is SubIrreFlexive & O is SubTransitive holds
O is asymmetric

proof end;

theorem Th37: :: OPOSET_1:37

for O being non empty RelStr st O is asymmetric holds
O is SubIrreFlexive

proof end;

theorem Th38: :: OPOSET_1:38

for O being non empty RelStr st O is reflexive & O is SubSymmetric holds
O is symmetric

proof end;

registration

cluster non empty reflexive SubSymmetric -> non empty symmetric OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is reflexive & b₁ is SubSymmetric holds
b₁ is symmetric ;
by Th38;

end;

theorem Th39: :: OPOSET_1:39

for O being non empty RelStr st O is reflexive & O is SubAntisymmetric holds
O is antisymmetric

proof end;

registration

cluster non empty reflexive SubAntisymmetric -> non empty antisymmetric OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is reflexive & b₁ is SubAntisymmetric holds
b₁ is antisymmetric ;
by Th39;

end;

theorem Th40: :: OPOSET_1:40

for O being non empty RelStr st O is reflexive & O is SubTransitive holds
O is transitive

proof end;

registration

cluster non empty reflexive SubTransitive -> non empty transitive OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is reflexive & b₁ is SubTransitive holds
b₁ is transitive ;
by Th40;

end;

theorem Th41: :: OPOSET_1:41

for O being non empty RelStr st O is irreflexive & O is SubTransitive holds
O is transitive

proof end;

registration

cluster non empty irreflexive SubTransitive -> non empty transitive OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is irreflexive & b₁ is SubTransitive holds
b₁ is transitive ;
by Th41;

end;

theorem Th42: :: OPOSET_1:42

for O being non empty RelStr st O is irreflexive & O is asymmetric holds
O is Asymmetric

proof end;

registration

cluster non empty asymmetric irreflexive -> non empty Asymmetric OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is irreflexive & b₁ is asymmetric holds
b₁ is Asymmetric ;
by Th42;

end;

definition

let O be non empty RelStr ;
canceled;
attr O is SubQuasiOrdered means :Def21: :: OPOSET_1:def 21
( O is SubReFlexive & O is SubTransitive );

end;

:: deftheorem OPOSET_1:def 20 :

canceled;

:: deftheorem Def21 defines SubQuasiOrdered OPOSET_1:def 21 :

for O being non empty RelStr holds
( O is SubQuasiOrdered iff ( O is SubReFlexive & O is SubTransitive ) );

notation

let O be non empty RelStr ;
synonym SubPreOrdered O for SubQuasiOrdered ;

end;

definition

let O be non empty RelStr ;
attr O is QuasiOrdered means :Def22: :: OPOSET_1:def 22
( O is reflexive & O is transitive );

end;

:: deftheorem Def22 defines QuasiOrdered OPOSET_1:def 22 :

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 Th43: :: OPOSET_1:43

for O being non empty RelStr st O is QuasiOrdered holds
O is SubQuasiOrdered

proof end;

registration

cluster non empty QuasiOrdered -> non empty SubQuasiOrdered OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is QuasiOrdered holds
b₁ is SubQuasiOrdered ;
by Th43;

end;

registration

cluster TrivOrthoRelStr -> strict QuasiOrdered ;
coherence
TrivOrthoRelStr is QuasiOrdered by Def22;

end;

definition

let O be non empty OrthoRelStr ;
attr O is QuasiPure means :Def23: :: OPOSET_1:def 23
( O is Dneg & O is QuasiOrdered );

end;

:: deftheorem Def23 defines QuasiPure OPOSET_1:def 23 :

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 OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is QuasiPure & b₁ is Dneg & b₁ is QuasiOrdered & b₁ is strict )

proof end;

end;

registration

cluster TrivOrthoRelStr -> strict QuasiPure ;
coherence
TrivOrthoRelStr is QuasiPure by Def23;

end;

definition

mode QuasiPureOrthoRelStr is non empty QuasiPure OrthoRelStr ;

end;

definition

let O be non empty OrthoRelStr ;
attr O is SubPartialOrdered means :Def24: :: OPOSET_1:def 24
( O is reflexive & O is SubAntisymmetric & O is SubTransitive );

end;

:: deftheorem Def24 defines SubPartialOrdered OPOSET_1:def 24 :

for O being non empty OrthoRelStr holds
( O is SubPartialOrdered iff ( O is reflexive & O is SubAntisymmetric & O is SubTransitive ) );

definition

let O be non empty OrthoRelStr ;
attr O is PartialOrdered means :Def25: :: OPOSET_1:def 25
( O is reflexive & O is antisymmetric & O is transitive );

end;

:: deftheorem Def25 defines PartialOrdered OPOSET_1:def 25 :

for O being non empty OrthoRelStr holds
( O is PartialOrdered iff ( O is reflexive & O is antisymmetric & O is transitive ) );

theorem Th44: :: OPOSET_1:44

for O being non empty OrthoRelStr holds
( O is SubPartialOrdered iff O is PartialOrdered )

proof end;

registration

cluster non empty SubPartialOrdered -> non empty PartialOrdered OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is SubPartialOrdered holds
b₁ is PartialOrdered by Th44;
cluster non empty PartialOrdered -> non empty SubPartialOrdered OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is PartialOrdered holds
b₁ is SubPartialOrdered by Th44;

end;

registration

cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is PartialOrdered holds
( b₁ is reflexive & b₁ is antisymmetric & b₁ is transitive ) by Def25;
cluster non empty reflexive transitive antisymmetric -> non empty PartialOrdered OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is reflexive & b₁ is antisymmetric & b₁ is transitive holds
b₁ is PartialOrdered by Def25;

end;

definition

let O be non empty OrthoRelStr ;
attr O is Pure means :Def26: :: OPOSET_1:def 26
( O is Dneg & O is PartialOrdered );

end;

:: deftheorem Def26 defines Pure OPOSET_1:def 26 :

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 OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is Pure & b₁ is Dneg & b₁ is PartialOrdered & b₁ is strict )

proof end;

end;

registration

cluster TrivOrthoRelStr -> strict Pure ;
coherence
TrivOrthoRelStr is Pure by Def26;

end;

definition

mode PureOrthoRelStr is non empty Pure OrthoRelStr ;

end;

definition

let O be non empty OrthoRelStr ;
attr O is SubStrictPartialOrdered means :Def27: :: OPOSET_1:def 27
( O is asymmetric & O is SubTransitive );

end;

:: deftheorem Def27 defines SubStrictPartialOrdered OPOSET_1:def 27 :

for O being non empty OrthoRelStr holds
( O is SubStrictPartialOrdered iff ( O is asymmetric & O is SubTransitive ) );

definition

let O be non empty OrthoRelStr ;
attr O is StrictPartialOrdered means :Def28: :: OPOSET_1:def 28
( O is Asymmetric & O is transitive );

end;

:: deftheorem Def28 defines StrictPartialOrdered OPOSET_1:def 28 :

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 Th45: :: OPOSET_1:45

for O being non empty OrthoRelStr st O is StrictPartialOrdered holds
O is SubStrictPartialOrdered

proof end;

registration

cluster non empty StrictPartialOrdered -> non empty SubStrictPartialOrdered OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is StrictPartialOrdered holds
b₁ is SubStrictPartialOrdered by Th45;

end;

theorem Th46: :: OPOSET_1:46

for O being non empty OrthoRelStr st O is SubStrictPartialOrdered holds
O is SubIrreFlexive

proof end;

registration

cluster non empty SubStrictPartialOrdered -> non empty SubIrreFlexive OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is SubStrictPartialOrdered holds
b₁ is SubIrreFlexive by Th46;

end;

theorem Th47: :: OPOSET_1:47

for O being non empty OrthoRelStr st O is irreflexive & O is SubStrictPartialOrdered holds
O is StrictPartialOrdered

proof end;

registration

cluster non empty irreflexive SubStrictPartialOrdered -> non empty StrictPartialOrdered OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is irreflexive & b₁ is SubStrictPartialOrdered holds
b₁ is StrictPartialOrdered by Th47;

end;

theorem Th48: :: OPOSET_1:48

for O being non empty OrthoRelStr st O is StrictPartialOrdered holds
O is irreflexive

proof end;

registration

cluster non empty StrictPartialOrdered -> non empty irreflexive OrthoRelStr ;
coherence
for b₁ being non empty OrthoRelStr st b₁ is StrictPartialOrdered holds
b₁ is irreflexive by Th48;

end;

registration

cluster TrivAsymOrthoRelStr -> irreflexive strict StrictPartialOrdered ;
coherence
( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is StrictPartialOrdered ) by Def28;

end;

registration

cluster non empty irreflexive strict StrictPartialOrdered OrthoRelStr ;
existence
ex b₁ being non empty strict OrthoRelStr st
( b₁ is irreflexive & b₁ is StrictPartialOrdered )

proof end;

end;

theorem :: OPOSET_1:49

for QO being non empty QuasiOrdered OrthoRelStr st QO is SubAntisymmetric holds
QO is PartialOrdered

proof end;

registration

cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric OrthoRelStr ;
correctness
coherence
for b₁ being non empty OrthoRelStr st b₁ is PartialOrdered holds
( b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric );
;

end;

definition

let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
canceled;
canceled;
canceled;
attr f is Orderinvolutive means :Def32: :: OPOSET_1:def 32
ex g being Function of PO,PO st
( g = f & g is dneg & g is antitone );

end;

:: deftheorem OPOSET_1:def 29 :

canceled;

:: deftheorem OPOSET_1:def 30 :

canceled;

:: deftheorem OPOSET_1:def 31 :

canceled;

:: deftheorem Def32 defines Orderinvolutive OPOSET_1:def 32 :

for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f is Orderinvolutive iff ex g being Function of PO,PO st
( g = f & g is dneg & g is antitone ) );

definition

let PO be non empty OrthoRelStr ;
attr PO is OrderInvolutive means :Def33: :: OPOSET_1:def 33
ex f being Function of PO,PO st
( f = the Compl of PO & f is Orderinvolutive );

end;

:: deftheorem Def33 defines OrderInvolutive OPOSET_1:def 33 :

for PO being non empty OrthoRelStr holds
( PO is OrderInvolutive iff ex f being Function of PO,PO st
( f = the Compl of PO & f is Orderinvolutive ) );

theorem :: OPOSET_1:50

canceled;

theorem Th51: :: OPOSET_1:51

the Compl of TrivOrthoRelStr is Orderinvolutive

proof end;

registration

cluster TrivOrthoRelStr -> strict OrderInvolutive ;
coherence
TrivOrthoRelStr is OrderInvolutive by Def33, Th51;

end;

registration

cluster non empty PartialOrdered Pure OrderInvolutive OrthoRelStr ;
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is OrderInvolutive & b₁ is Pure & b₁ is PartialOrdered )

proof 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;
pred f QuasiOrthoComplement_on PO means :Def34: :: OPOSET_1:def 34
( 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 Def34 defines QuasiOrthoComplement_on OPOSET_1:def 34 :

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 ;
attr PO is QuasiOrthocomplemented means :Def35: :: OPOSET_1:def 35
ex f being Function of PO,PO st
( f = the Compl of PO & f QuasiOrthoComplement_on PO );

end;

:: deftheorem Def35 defines QuasiOrthocomplemented OPOSET_1:def 35 :

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

theorem Th52: :: OPOSET_1:52

TrivOrthoRelStr is QuasiOrthocomplemented

proof end;

definition

let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
pred f OrthoComplement_on PO means :Def36: :: OPOSET_1:def 36
( 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 Def36 defines OrthoComplement_on OPOSET_1:def 36 :

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 ;
attr PO is Orthocomplemented means :Def37: :: OPOSET_1:def 37
ex f being Function of PO,PO st
( f = the Compl of PO & f OrthoComplement_on PO );

end;

:: deftheorem Def37 defines Orthocomplemented OPOSET_1:def 37 :

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

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

theorem Th54: :: OPOSET_1:54

TrivOrthoRelStr is Orthocomplemented

proof end;

registration

cluster TrivOrthoRelStr -> strict QuasiOrthocomplemented Orthocomplemented ;
coherence
( TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is Orthocomplemented ) by Th52, Th54;

end;

registration

cluster non empty PartialOrdered QuasiOrthocomplemented Orthocomplemented OrthoRelStr ;
correctness
existence
ex b₁ being non empty OrthoRelStr st
( b₁ is Orthocomplemented & b₁ is QuasiOrthocomplemented & b₁ is PartialOrdered );

proof end;

end;

definition

mode QuasiOrthoPoset is non empty PartialOrdered QuasiOrthocomplemented OrthoRelStr ;
mode OrthoPoset is non empty PartialOrdered Orthocomplemented OrthoRelStr ;

end;