:: OPOSET_1 semantic presentation

definition

attr a₁ is strict;
struct OrthoRelStr -> RelStr , ComplStr ;
aggr OrthoRelStr(# carrier, InternalRel, Compl #) -> OrthoRelStr ;

end;

definition

let c₁, c₂ be set ;
func {} c₁,c₂ -> Relation of a₁,a₂ equals :: OPOSET_1:def 1
{} ;
correctness by RELSET_1:25;
func [#] c₁,c₂ -> Relation of a₁,a₂ equals :: OPOSET_1:def 2
[:a₁,a₂:];
correctness by RELSET_1:def 1;

end;

:: deftheorem Def1 defines {} OPOSET_1:def 1 :

:: deftheorem Def2 defines [#] OPOSET_1:def 2 :

theorem Th1: :: OPOSET_1:1

for b₁ being non empty set holds field (id b₁) = b₁

proof end;

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

theorem Th2: :: OPOSET_1:2

canceled;

theorem Th3: :: OPOSET_1:3

op1 = {[{} ,{} ]}

proof end;

theorem Th4: :: OPOSET_1:4

for b₁ being non empty reflexive antisymmetric RelStr
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
( sup {b₂,b₃} = b₃ & inf {b₂,b₃} = b₂ )

proof end;

theorem Th5: :: OPOSET_1:5

canceled;

theorem Th6: :: OPOSET_1:6

for b₁, b₂ being set holds field ({} b₁,b₂) = {}

proof end;

theorem Th7: :: OPOSET_1:7

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ holds
( b₂ is reflexive & field b₂ = b₁ )

proof end;

theorem Th8: :: OPOSET_1:8

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_symmetric_in b₁ holds
b₂ is symmetric

proof end;

theorem Th9: :: OPOSET_1:9

for b₁, b₂ being non empty set
for b₃ being Relation of b₁ st b₃ is symmetric & field b₃ c= b₂ holds
b₃ is_symmetric_in b₂

proof end;

theorem Th10: :: OPOSET_1:10

for b₁, b₂ being non empty set
for b₃ being Relation of b₁ st b₃ is antisymmetric & field b₃ c= b₂ holds
b₃ is_antisymmetric_in b₂

proof end;

theorem Th11: :: OPOSET_1:11

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_antisymmetric_in b₁ holds
b₂ is antisymmetric

proof end;

theorem Th12: :: OPOSET_1:12

for b₁, b₂ being non empty set
for b₃ being Relation of b₁ st b₃ is transitive & field b₃ c= b₂ holds
b₃ is_transitive_in b₂

proof end;

theorem Th13: :: OPOSET_1:13

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_transitive_in b₁ holds
b₂ is transitive

proof end;

theorem Th14: :: OPOSET_1:14

for b₁, b₂ being non empty set
for b₃ being Relation of b₁ st b₃ is asymmetric & field b₃ c= b₂ holds
b₃ is_asymmetric_in b₂

proof end;

theorem Th15: :: OPOSET_1:15

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_asymmetric_in b₁ holds
b₂ is asymmetric

proof end;

theorem Th16: :: OPOSET_1:16

for b₁, b₂ being non empty set
for b₃ being Relation of b₁ st b₃ is irreflexive & field b₃ c= b₂ holds
b₃ is_irreflexive_in b₂

proof end;

theorem Th17: :: OPOSET_1:17

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_irreflexive_in b₁ holds
b₂ is irreflexive

proof end;

registration

let c₁ be set ;
cluster irreflexive asymmetric transitive Relation of a₁,a₁;
existence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be Relation of c₁;
let c₃ be UnOp of c₁;
cluster OrthoRelStr(# a₁,a₂,a₃ #) -> non empty ;
coherence

proof end;

end;

registration

cluster non empty strict OrthoRelStr ;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Function of c₁,c₁;
attr a₂ is dneg means :Def3: :: OPOSET_1:def 3
for b₁ being Element of a₁ holds a₂ . (a₂ . b₁) = b₁;

end;

:: deftheorem Def3 defines dneg OPOSET_1:def 3 :

notation

let c₁ be non empty set ;
let c₂ be Function of c₁,c₁;
synonym involutive c₂ for dneg c₂;

end;

theorem Th18: :: OPOSET_1:18

canceled;

theorem Th19: :: OPOSET_1:19

op1 is dneg

proof end;

theorem Th20: :: OPOSET_1:20

for b₁ being non empty set holds id b₁ is dneg

proof end;

registration

let c₁ be non empty OrthoRelStr ;
cluster dneg Relation of the carrier of a₁,the carrier of a₁;
existence

proof end;

end;

definition

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

end;

:: deftheorem Def4 defines TrivOrthoRelStr OPOSET_1:def 4 :

notation

synonym TrivPoset for TrivOrthoRelStr ;

end;

Lemma20: TrivOrthoRelStr is trivial

proof end;

registration

cluster TrivOrthoRelStr -> non empty trivial strict ;
coherence by Lemma20;

end;

definition

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

end;

:: deftheorem Def5 defines TrivAsymOrthoRelStr OPOSET_1:def 5 :

registration

cluster TrivAsymOrthoRelStr -> non empty strict ;
coherence ;

end;

definition

let c₁ be non empty OrthoRelStr ;
attr a₁ is Dneg means :Def6: :: OPOSET_1:def 6
ex b₁ being Function of a₁,a₁ st
( b₁ = the Compl of a₁ & b₁ is dneg );

end;

:: deftheorem Def6 defines Dneg OPOSET_1:def 6 :

theorem Th21: :: OPOSET_1:21

TrivOrthoRelStr is Dneg by Def6, Th19;

registration

cluster TrivOrthoRelStr -> non empty trivial strict Dneg ;
coherence by Def6, Th19;

end;

registration

cluster non empty Dneg OrthoRelStr ;
existence by Def4;

end;

definition

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

end;

:: deftheorem Def7 OPOSET_1:def 7 :

:: deftheorem Def8 OPOSET_1:def 8 :

:: deftheorem Def9 defines SubReFlexive OPOSET_1:def 9 :

theorem Th22: :: OPOSET_1:22

for b₁ being non empty RelStr st b₁ is reflexive holds
b₁ is SubReFlexive

proof end;

theorem Th23: :: OPOSET_1:23

TrivOrthoRelStr is reflexive

proof end;

registration

cluster TrivOrthoRelStr -> non empty reflexive trivial strict Dneg ;
coherence by Th23;

end;

registration

cluster non empty reflexive strict OrthoRelStr ;
existence by Th23;

end;

definition

let c₁ be non empty RelStr ;
canceled;
attr a₁ is SubIrreFlexive means :Def11: :: OPOSET_1:def 11
the InternalRel of a₁ is irreflexive;
redefine attr a₁ is irreflexive means :Def12: :: OPOSET_1:def 12
the InternalRel of a₁ is_irreflexive_in the carrier of a₁;
compatibility

proof end;

end;

:: deftheorem Def10 OPOSET_1:def 10 :

:: deftheorem Def11 defines SubIrreFlexive OPOSET_1:def 11 :

:: deftheorem Def12 defines irreflexive OPOSET_1:def 12 :

theorem Th24: :: OPOSET_1:24

for b₁ being non empty RelStr st b₁ is irreflexive holds
b₁ is SubIrreFlexive

proof end;

theorem Th25: :: OPOSET_1:25

TrivAsymOrthoRelStr is irreflexive

proof end;

registration

cluster non empty irreflexive -> non empty SubIrreFlexive OrthoRelStr ;
correctness by Th24;

end;

registration

cluster TrivAsymOrthoRelStr -> non empty irreflexive strict SubIrreFlexive ;
coherence by Th25;

end;

registration

cluster non empty irreflexive strict SubIrreFlexive OrthoRelStr ;
existence by Th25;

end;

definition

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

end;

:: deftheorem Def13 defines SubSymmetric OPOSET_1:def 13 :

theorem Th26: :: OPOSET_1:26

for b₁ being non empty RelStr st b₁ is symmetric holds
b₁ is SubSymmetric

proof end;

theorem Th27: :: OPOSET_1:27

TrivOrthoRelStr is symmetric

proof end;

registration

cluster non empty symmetric -> non empty SubSymmetric OrthoRelStr ;
correctness by Th26;

end;

registration

cluster non empty symmetric strict SubSymmetric OrthoRelStr ;
existence by Th27;

end;

definition

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

end;

:: deftheorem Def14 OPOSET_1:def 14 :

:: deftheorem Def15 defines SubAntisymmetric OPOSET_1:def 15 :

theorem Th28: :: OPOSET_1:28

for b₁ being non empty RelStr st b₁ is antisymmetric holds
b₁ is SubAntisymmetric

proof end;

Lemma33: TrivOrthoRelStr is antisymmetric
;

registration

cluster non empty antisymmetric -> non empty SubAntisymmetric OrthoRelStr ;
correctness by Th28;

end;

registration

cluster TrivOrthoRelStr -> non empty reflexive symmetric trivial strict Dneg SubSymmetric SubAntisymmetric ;
coherence by Th27;

end;

registration

cluster non empty antisymmetric symmetric strict SubSymmetric SubAntisymmetric OrthoRelStr ;
existence by Lemma33;

end;

definition

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

end;

:: deftheorem Def16 OPOSET_1:def 16 :

:: deftheorem Def17 OPOSET_1:def 17 :

:: deftheorem Def18 defines Asymmetric OPOSET_1:def 18 :

theorem Th29: :: OPOSET_1:29

canceled;

theorem Th30: :: OPOSET_1:30

for b₁ being non empty RelStr st b₁ is Asymmetric holds
b₁ is asymmetric

proof end;

theorem Th31: :: OPOSET_1:31

TrivAsymOrthoRelStr is Asymmetric

proof end;

registration

cluster non empty Asymmetric -> non empty asymmetric OrthoRelStr ;
correctness by Th30;

end;

registration

cluster TrivAsymOrthoRelStr -> non empty asymmetric irreflexive strict SubIrreFlexive Asymmetric ;
coherence by Th31;

end;

registration

cluster non empty asymmetric strict Asymmetric OrthoRelStr ;
existence by Th31;

end;

definition

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

end;

:: deftheorem Def19 defines SubTransitive OPOSET_1:def 19 :

theorem Th32: :: OPOSET_1:32

for b₁ being non empty RelStr st b₁ is transitive holds
b₁ is SubTransitive

proof end;

registration

cluster non empty transitive -> non empty SubTransitive OrthoRelStr ;
correctness by Th32;

end;

registration

cluster non empty reflexive transitive antisymmetric symmetric strict SubSymmetric SubAntisymmetric SubTransitive OrthoRelStr ;
existence by Lemma33;

end;

theorem Th33: :: OPOSET_1:33

canceled;

theorem Th34: :: OPOSET_1:34

TrivAsymOrthoRelStr is transitive

proof end;

registration

cluster TrivAsymOrthoRelStr -> non empty transitive asymmetric irreflexive strict SubIrreFlexive Asymmetric SubTransitive ;
coherence by Th34;

end;

registration

cluster non empty transitive asymmetric irreflexive strict SubIrreFlexive Asymmetric SubTransitive OrthoRelStr ;
existence by Th25;

end;

theorem Th35: :: OPOSET_1:35

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

proof end;

theorem Th36: :: OPOSET_1:36

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

proof end;

theorem Th37: :: OPOSET_1:37

for b₁ being non empty RelStr st b₁ is asymmetric holds
b₁ is SubIrreFlexive

proof end;

theorem Th38: :: OPOSET_1:38

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

proof end;

registration

cluster non empty reflexive SubSymmetric -> non empty symmetric SubSymmetric OrthoRelStr ;
correctness by Th38;

end;

theorem Th39: :: OPOSET_1:39

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

proof end;

registration

cluster non empty reflexive SubAntisymmetric -> non empty antisymmetric SubAntisymmetric OrthoRelStr ;
correctness by Th39;

end;

theorem Th40: :: OPOSET_1:40

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

proof end;

registration

cluster non empty reflexive SubTransitive -> non empty transitive SubTransitive OrthoRelStr ;
correctness by Th40;

end;

theorem Th41: :: OPOSET_1:41

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

proof end;

registration

cluster non empty irreflexive SubTransitive -> non empty transitive SubTransitive OrthoRelStr ;
correctness by Th41;

end;

theorem Th42: :: OPOSET_1:42

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

proof end;

registration

cluster non empty asymmetric irreflexive -> non empty asymmetric Asymmetric OrthoRelStr ;
correctness by Th42;

end;

definition

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

end;

:: deftheorem Def20 OPOSET_1:def 20 :

:: deftheorem Def21 defines SubQuasiOrdered OPOSET_1:def 21 :

notation

let c₁ be non empty RelStr ;
synonym SubPreOrdered c₁ for SubQuasiOrdered c₁;

end;

definition

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

end;

:: deftheorem Def22 defines QuasiOrdered OPOSET_1:def 22 :

notation

let c₁ be non empty RelStr ;
synonym PreOrdered c₁ for QuasiOrdered c₁;

end;

theorem Th43: :: OPOSET_1:43

for b₁ being non empty RelStr st b₁ is QuasiOrdered holds
b₁ is SubQuasiOrdered

proof end;

registration

cluster non empty QuasiOrdered -> non empty SubQuasiOrdered OrthoRelStr ;
correctness by Th43;

end;

registration

cluster TrivOrthoRelStr -> non empty reflexive symmetric trivial strict Dneg SubSymmetric SubAntisymmetric SubTransitive SubQuasiOrdered QuasiOrdered ;
coherence by Def22;

end;

definition

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

end;

:: deftheorem Def23 defines QuasiPure OPOSET_1:def 23 :

registration

cluster non empty strict Dneg SubQuasiOrdered QuasiOrdered QuasiPure OrthoRelStr ;
existence

proof end;

end;

registration

cluster TrivOrthoRelStr -> non empty reflexive symmetric trivial strict Dneg SubSymmetric SubAntisymmetric SubTransitive SubQuasiOrdered QuasiOrdered QuasiPure ;
coherence by Def23;

end;

definition

mode QuasiPureOrthoRelStr is non empty QuasiPure OrthoRelStr ;

end;

definition

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

end;

:: deftheorem Def24 defines SubPartialOrdered OPOSET_1:def 24 :

definition

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

end;

:: deftheorem Def25 defines PartialOrdered OPOSET_1:def 25 :

theorem Th44: :: OPOSET_1:44

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

proof end;

registration

cluster non empty SubPartialOrdered -> non empty PartialOrdered OrthoRelStr ;
coherence by Th44;
cluster non empty PartialOrdered -> non empty SubPartialOrdered OrthoRelStr ;
coherence by Th44;

end;

registration

cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric SubAntisymmetric SubTransitive OrthoRelStr ;
coherence by Def25;
cluster non empty reflexive transitive antisymmetric -> non empty SubPartialOrdered PartialOrdered OrthoRelStr ;
coherence by Def25;

end;

definition

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

end;

:: deftheorem Def26 defines Pure OPOSET_1:def 26 :

registration

cluster non empty reflexive transitive antisymmetric strict Dneg SubAntisymmetric SubTransitive SubPartialOrdered PartialOrdered Pure OrthoRelStr ;
existence

proof end;

end;

registration end;

definition

mode PureOrthoRelStr is non empty Pure OrthoRelStr ;

end;

definition

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

end;

:: deftheorem Def27 defines SubStrictPartialOrdered OPOSET_1:def 27 :

definition

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

end;

:: deftheorem Def28 defines StrictPartialOrdered OPOSET_1:def 28 :

notation

let c₁ be non empty OrthoRelStr ;
synonym StrictOrdered c₁ for StrictPartialOrdered c₁;

end;

theorem Th45: :: OPOSET_1:45

for b₁ being non empty OrthoRelStr st b₁ is StrictPartialOrdered holds
b₁ is SubStrictPartialOrdered

proof end;

registration

cluster non empty StrictPartialOrdered -> non empty SubStrictPartialOrdered OrthoRelStr ;
coherence by Th45;

end;

theorem Th46: :: OPOSET_1:46

for b₁ being non empty OrthoRelStr st b₁ is SubStrictPartialOrdered holds
b₁ is SubIrreFlexive

proof end;

registration

cluster non empty SubStrictPartialOrdered -> non empty SubIrreFlexive OrthoRelStr ;
coherence by Th46;

end;

theorem Th47: :: OPOSET_1:47

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

proof end;

registration

cluster non empty irreflexive SubStrictPartialOrdered -> non empty SubIrreFlexive SubStrictPartialOrdered StrictPartialOrdered OrthoRelStr ;
coherence by Th47;

end;

theorem Th48: :: OPOSET_1:48

for b₁ being non empty OrthoRelStr st b₁ is StrictPartialOrdered holds
b₁ is irreflexive

proof end;

registration

cluster non empty StrictPartialOrdered -> non empty irreflexive SubIrreFlexive OrthoRelStr ;
coherence by Th48;

end;

registration

cluster TrivAsymOrthoRelStr -> non empty transitive asymmetric irreflexive strict SubIrreFlexive Asymmetric SubTransitive SubStrictPartialOrdered StrictPartialOrdered ;
coherence by Def28;

end;

registration

cluster non empty irreflexive strict SubIrreFlexive SubStrictPartialOrdered StrictPartialOrdered OrthoRelStr ;
existence

proof end;

end;

theorem Th49: :: OPOSET_1:49

for b₁ being non empty QuasiOrdered OrthoRelStr st b₁ is SubAntisymmetric holds
b₁ is PartialOrdered

proof end;

Lemma60: for b₁ being non empty PartialOrdered OrthoRelStr holds b₁ is Poset
;

registration

cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric SubAntisymmetric SubTransitive SubPartialOrdered PartialOrdered OrthoRelStr ;
correctness by Lemma60;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be UnOp of the carrier of c₁;
canceled;
canceled;
canceled;
attr a₂ is Orderinvolutive means :Def32: :: OPOSET_1:def 32
ex b₁ being Function of a₁,a₁ st
( b₁ = a₂ & b₁ is dneg & b₁ is antitone );

end;

:: deftheorem Def29 OPOSET_1:def 29 :

:: deftheorem Def30 OPOSET_1:def 30 :

:: deftheorem Def31 OPOSET_1:def 31 :

:: deftheorem Def32 defines Orderinvolutive OPOSET_1:def 32 :

definition

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

end;

:: deftheorem Def33 defines OrderInvolutive OPOSET_1:def 33 :

theorem Th50: :: OPOSET_1:50

canceled;

theorem Th51: :: OPOSET_1:51

the Compl of TrivOrthoRelStr is Orderinvolutive

proof end;

registration end;

registration

cluster non empty reflexive transitive antisymmetric SubAntisymmetric SubTransitive SubPartialOrdered PartialOrdered Pure OrderInvolutive OrthoRelStr ;
existence

proof end;

end;

definition

mode PreOrthoPoset is non empty PartialOrdered Pure OrderInvolutive OrthoRelStr ;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be UnOp of the carrier of c₁;
pred c₂ QuasiOrthoComplement_on c₁ means :Def34: :: OPOSET_1:def 34
( a₂ is Orderinvolutive & ( for b₁ being Element of a₁ holds
( ex_sup_of {b₁,(a₂ . b₁)},a₁ & ex_inf_of {b₁,(a₂ . b₁)},a₁ ) ) );

end;

:: deftheorem Def34 defines QuasiOrthoComplement_on OPOSET_1:def 34 :

definition

let c₁ be non empty OrthoRelStr ;
attr a₁ is QuasiOrthocomplemented means :Def35: :: OPOSET_1:def 35
ex b₁ being Function of a₁,a₁ st
( b₁ = the Compl of a₁ & b₁ QuasiOrthoComplement_on a₁ );

end;

:: deftheorem Def35 defines QuasiOrthocomplemented OPOSET_1:def 35 :

theorem Th52: :: OPOSET_1:52

TrivOrthoRelStr is QuasiOrthocomplemented

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be UnOp of the carrier of c₁;
pred c₂ OrthoComplement_on c₁ means :Def36: :: OPOSET_1:def 36
( a₂ is Orderinvolutive & ( for b₁ being Element of a₁ holds
( ex_sup_of {b₁,(a₂ . b₁)},a₁ & ex_inf_of {b₁,(a₂ . b₁)},a₁ & "\/" {b₁,(a₂ . b₁)},a₁ is_maximum_of the carrier of a₁ & "/\" {b₁,(a₂ . b₁)},a₁ is_minimum_of the carrier of a₁ ) ) );

end;

:: deftheorem Def36 defines OrthoComplement_on OPOSET_1:def 36 :

definition

let c₁ be non empty OrthoRelStr ;
attr a₁ is Orthocomplemented means :Def37: :: OPOSET_1:def 37
ex b₁ being Function of a₁,a₁ st
( b₁ = the Compl of a₁ & b₁ OrthoComplement_on a₁ );

end;

:: deftheorem Def37 defines Orthocomplemented OPOSET_1:def 37 :

theorem Th53: :: OPOSET_1:53

for b₁ being non empty OrthoRelStr
for b₂ being UnOp of the carrier of b₁ st b₂ OrthoComplement_on b₁ holds
b₂ QuasiOrthoComplement_on b₁

proof end;

theorem Th54: :: OPOSET_1:54

TrivOrthoRelStr is Orthocomplemented

proof end;

registration end;

registration

cluster non empty reflexive transitive antisymmetric SubAntisymmetric SubTransitive SubPartialOrdered PartialOrdered QuasiOrthocomplemented Orthocomplemented OrthoRelStr ;
correctness

proof end;

end;

definition

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

end;