begin
:: deftheorem defines {} OPOSET_1:def 1 :
:: deftheorem OPOSET_1:def 2 :
canceled;
theorem
Lm1:
id {{} } = {[{} ,{} ]}
by SYSREL:30;
theorem
canceled;
theorem Th3:
theorem
theorem
canceled;
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem Def3 defines dneg OPOSET_1:def 3 :
theorem
canceled;
theorem Th19:
theorem Th20:
:: deftheorem Def4 defines TrivOrthoRelStr OPOSET_1:def 4 :
:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 5 :
:: deftheorem Def6 defines Dneg OPOSET_1:def 6 :
theorem
:: deftheorem OPOSET_1:def 7 :
canceled;
:: deftheorem OPOSET_1:def 8 :
canceled;
:: deftheorem Def9 defines SubReFlexive OPOSET_1:def 9 :
theorem
theorem Th23:
:: deftheorem OPOSET_1:def 10 :
canceled;
:: deftheorem Def11 defines SubIrreFlexive OPOSET_1:def 11 :
:: deftheorem Def12 defines irreflexive OPOSET_1:def 12 :
theorem Th24:
theorem Th25:
:: deftheorem Def13 defines SubSymmetric OPOSET_1:def 13 :
theorem Th26:
theorem Th27:
:: deftheorem OPOSET_1:def 14 :
canceled;
:: deftheorem Def15 defines SubAntisymmetric OPOSET_1:def 15 :
theorem Th28:
Lm2:
TrivOrthoRelStr is antisymmetric
;
:: deftheorem OPOSET_1:def 16 :
canceled;
:: deftheorem OPOSET_1:def 17 :
canceled;
:: deftheorem Def18 defines Asymmetric OPOSET_1:def 18 :
theorem
canceled;
theorem Th30:
theorem Th31:
:: deftheorem Def19 defines SubTransitive OPOSET_1:def 19 :
theorem Th32:
theorem
canceled;
theorem Th34:
theorem
theorem
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
begin
:: deftheorem OPOSET_1:def 20 :
canceled;
:: deftheorem Def21 defines SubQuasiOrdered OPOSET_1:def 21 :
:: deftheorem Def22 defines QuasiOrdered OPOSET_1:def 22 :
theorem Th43:
:: 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:
:: 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:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
:: 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
canceled;
theorem Th51:
:: deftheorem Def34 defines QuasiOrthoComplement_on OPOSET_1:def 34 :
:: deftheorem Def35 defines QuasiOrthocomplemented OPOSET_1:def 35 :
theorem Th52:
:: deftheorem Def36 defines OrthoComplement_on OPOSET_1:def 36 :
:: deftheorem Def37 defines Orthocomplemented OPOSET_1:def 37 :
theorem
theorem Th54: