:: OPOSET_1 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem defines {} OPOSET_1:def 1 :
:: deftheorem defines [#] OPOSET_1:def 2 :
theorem Th1: :: OPOSET_1:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm1:
id {{} } = {[{} ,{} ]}
by SYSREL:30;
theorem :: OPOSET_1:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th3: :: OPOSET_1:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: OPOSET_1:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: OPOSET_1:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th6: :: OPOSET_1:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: OPOSET_1:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th8: :: OPOSET_1:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: OPOSET_1:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: OPOSET_1:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th11: :: OPOSET_1:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: OPOSET_1:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: OPOSET_1:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: OPOSET_1:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: OPOSET_1:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: OPOSET_1:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: OPOSET_1:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def3 defines dneg OPOSET_1:def 3 :
theorem :: OPOSET_1:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th19: :: OPOSET_1:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: OPOSET_1:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def4 defines TrivOrthoRelStr OPOSET_1:def 4 :
Lm2:
TrivOrthoRelStr is trivial
:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 5 :
:: deftheorem Def6 defines Dneg OPOSET_1:def 6 :
theorem :: OPOSET_1:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem OPOSET_1:def 7 :
canceled;
:: deftheorem OPOSET_1:def 8 :
canceled;
:: deftheorem Def9 defines SubReFlexive OPOSET_1:def 9 :
theorem :: OPOSET_1:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th23: :: OPOSET_1:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem OPOSET_1:def 10 :
canceled;
:: deftheorem Def11 defines SubIrreFlexive OPOSET_1:def 11 :
:: deftheorem Def12 defines irreflexive OPOSET_1:def 12 :
theorem Th24: :: OPOSET_1:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: OPOSET_1:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def13 defines SubSymmetric OPOSET_1:def 13 :
theorem Th26: :: OPOSET_1:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th27: :: OPOSET_1:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem OPOSET_1:def 14 :
canceled;
:: deftheorem Def15 defines SubAntisymmetric OPOSET_1:def 15 :
theorem Th28: :: OPOSET_1:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm3:
TrivOrthoRelStr is antisymmetric
;
:: deftheorem OPOSET_1:def 16 :
canceled;
:: deftheorem OPOSET_1:def 17 :
canceled;
:: deftheorem Def18 defines Asymmetric OPOSET_1:def 18 :
theorem :: OPOSET_1:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th30: :: OPOSET_1:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th31: :: OPOSET_1:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def19 defines SubTransitive OPOSET_1:def 19 :
theorem Th32: :: OPOSET_1:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: OPOSET_1:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th34: :: OPOSET_1:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: OPOSET_1:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: OPOSET_1:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th37: :: OPOSET_1:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th38: :: OPOSET_1:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th39: :: OPOSET_1:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th40: :: OPOSET_1:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th41: :: OPOSET_1:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th42: :: OPOSET_1:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem OPOSET_1:def 20 :
canceled;
:: deftheorem Def21 defines SubQuasiOrdered OPOSET_1:def 21 :
:: deftheorem Def22 defines QuasiOrdered OPOSET_1:def 22 :
theorem Th43: :: OPOSET_1:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def23 defines QuasiPure OPOSET_1:def 23 :
:: deftheorem Def24 defines SubPartialOrdered OPOSET_1:def 24 :
:: deftheorem Def25 defines PartialOrdered OPOSET_1:def 25 :
theorem Th44: :: OPOSET_1:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def26 defines Pure OPOSET_1:def 26 :
:: deftheorem Def27 defines SubStrictPartialOrdered OPOSET_1:def 27 :
:: deftheorem Def28 defines StrictPartialOrdered OPOSET_1:def 28 :
theorem Th45: :: OPOSET_1:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th46: :: OPOSET_1:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th47: :: OPOSET_1:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th48: :: OPOSET_1:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: OPOSET_1:49
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm4:
for PO being non empty PartialOrdered OrthoRelStr holds PO is Poset
;
:: 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 :
:: deftheorem Def33 defines OrderInvolutive OPOSET_1:def 33 :
theorem :: OPOSET_1:50
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th51: :: OPOSET_1:51
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def34 defines QuasiOrthoComplement_on OPOSET_1:def 34 :
:: deftheorem Def35 defines QuasiOrthocomplemented OPOSET_1:def 35 :
theorem Th52: :: OPOSET_1:52
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def36 defines OrthoComplement_on OPOSET_1:def 36 :
:: deftheorem Def37 defines Orthocomplemented OPOSET_1:def 37 :
theorem :: OPOSET_1:53
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th54: :: OPOSET_1:54
:: Showing IDV graph ... (Click the Palm Tree again to close it) 