:: OPOSET_1 semantic presentation begin theorem :: OPOSET_1:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r3_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k1_yellow_0 :::"sup"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set ($#k2_yellow_0 :::"inf"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_2 :::"irreflexive"::: ) ($#v5_relat_2 :::"asymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "(" ($#k2_zfmisc_1 :::"[#]"::: ) "(" "X" "," "X" ")" ")" ))); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); let "C" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "X")); cluster (Set ($#g2_qmax_1 :::"OrthoRelStr"::: ) "(#" "X" "," "R" "," "C" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registrationlet "O" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1("O") bbbadV1_FUNCT_2("O" "," "O") ($#v1_partit_2 :::"involutive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set "(" ($#k2_zfmisc_1 :::"[#]"::: ) "(" "O" "," "O" ")" ")" ))); end; definitionfunc :::"TrivOrthoRelStr"::: -> ($#v3_qmax_1 :::"strict"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) equals :: OPOSET_1:def 1 (Set ($#g2_qmax_1 :::"OrthoRelStr"::: ) "(#" (Num 1) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Num 1) ")" ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivOrthoRelStr"::: OPOSET_1:def 1 : (Bool (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g2_qmax_1 :::"OrthoRelStr"::: ) "(#" (Num 1) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Num 1) ")" ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" )); notationsynonym :::"TrivPoset"::: for :::"TrivOrthoRelStr"::: ; end; registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v3_qmax_1 :::"strict"::: ) ; end; definitionfunc :::"TrivAsymOrthoRelStr"::: -> ($#v3_qmax_1 :::"strict"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) equals :: OPOSET_1:def 2 (Set ($#g2_qmax_1 :::"OrthoRelStr"::: ) "(#" (Num 1) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" ); end; :: deftheorem defines :::"TrivAsymOrthoRelStr"::: OPOSET_1:def 2 : (Bool (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g2_qmax_1 :::"OrthoRelStr"::: ) "(#" (Num 1) "," (Set "(" ($#k1_partit_2 :::"{}"::: ) "(" (Num 1) "," (Num 1) ")" ")" ) "," (Set ($#k8_funct_5 :::"op1"::: ) ) "#)" )); registration cluster (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_qmax_1 :::"strict"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "O" is :::"Dneg"::: means :: OPOSET_1:def 3 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "O" "," "O" "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "O")) & (Bool (Set (Var "f")) "is" bbbadV1_PARTIT_2()) ")" )); end; :: deftheorem defines :::"Dneg"::: OPOSET_1:def 3 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v1_oposet_1 :::"Dneg"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "O")) "," (Set (Var "O")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "O")))) & (Bool (Set (Var "f")) "is" bbbadV1_PARTIT_2()) ")" )) ")" )); registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v3_qmax_1 :::"strict"::: ) ($#v1_oposet_1 :::"Dneg"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_oposet_1 :::"Dneg"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "O" is :::"SubReFlexive"::: means :: OPOSET_1:def 4 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "O") "is" ($#v1_relat_2 :::"reflexive"::: ) ); end; :: deftheorem defines :::"SubReFlexive"::: OPOSET_1:def 4 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v2_oposet_1 :::"SubReFlexive"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "O"))) "is" ($#v1_relat_2 :::"reflexive"::: ) ) ")" )); theorem :: OPOSET_1:2 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v3_orders_2 :::"reflexive"::: ) )) "holds" (Bool (Set (Var "O")) "is" ($#v2_oposet_1 :::"SubReFlexive"::: ) )) ; theorem :: OPOSET_1:3 (Bool (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) "is" ($#v3_orders_2 :::"reflexive"::: ) ) ; registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v3_orders_2 :::"reflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "O" is :::"irreflexive"::: means :: OPOSET_1:def 5 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "O") "is" ($#v2_relat_2 :::"irreflexive"::: ) ); redefine attr "O" is :::"irreflexive"::: means :: OPOSET_1:def 6 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "O") ($#r2_relat_2 :::"is_irreflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O")); end; :: deftheorem defines :::"irreflexive"::: OPOSET_1:def 5 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v3_necklace :::"irreflexive"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "O"))) "is" ($#v2_relat_2 :::"irreflexive"::: ) ) ")" )); :: deftheorem defines :::"irreflexive"::: OPOSET_1:def 6 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v3_necklace :::"irreflexive"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "O"))) ($#r2_relat_2 :::"is_irreflexive_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "O")))) ")" )); theorem :: OPOSET_1:4 (Bool (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) "is" ($#v3_necklace :::"irreflexive"::: ) ) ; registration cluster (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) -> ($#v3_necklace :::"irreflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_necklace :::"irreflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "O" is :::"symmetric"::: means :: OPOSET_1:def 7 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "O") "is" ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O")); end; :: deftheorem defines :::"symmetric"::: OPOSET_1:def 7 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v1_necklace :::"symmetric"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "O"))) "is" ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "O")))) ")" )); theorem :: OPOSET_1:5 (Bool (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) "is" ($#v1_necklace :::"symmetric"::: ) ) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_necklace :::"symmetric"::: ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "O" is :::"antisymmetric"::: means :: OPOSET_1:def 8 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "O") "is" ($#v4_relat_2 :::"antisymmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O")); end; :: deftheorem defines :::"antisymmetric"::: OPOSET_1:def 8 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "O"))) "is" ($#v4_relat_2 :::"antisymmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "O")))) ")" )); registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v1_necklace :::"symmetric"::: ) ($#v3_qmax_1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_necklace :::"symmetric"::: ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "O" is :::"asymmetric"::: means :: OPOSET_1:def 9 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "O") ($#r5_relat_2 :::"is_asymmetric_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O")); end; :: deftheorem defines :::"asymmetric"::: OPOSET_1:def 9 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v2_necklace :::"asymmetric"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "O"))) ($#r5_relat_2 :::"is_asymmetric_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "O")))) ")" )); theorem :: OPOSET_1:6 (Bool (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) "is" ($#v2_necklace :::"asymmetric"::: ) ) ; registration cluster (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) -> ($#v2_necklace :::"asymmetric"::: ) ($#v3_qmax_1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_necklace :::"asymmetric"::: ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; redefine attr "O" is :::"transitive"::: means :: OPOSET_1:def 10 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "O") "is" ($#v8_relat_2 :::"transitive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "O")); end; :: deftheorem defines :::"transitive"::: OPOSET_1:def 10 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v4_orders_2 :::"transitive"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "O"))) "is" ($#v8_relat_2 :::"transitive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "O")))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v1_necklace :::"symmetric"::: ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; theorem :: OPOSET_1:7 (Bool (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) "is" ($#v4_orders_2 :::"transitive"::: ) ) ; registration cluster (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) -> ($#v4_orders_2 :::"transitive"::: ) ($#v2_necklace :::"asymmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v2_necklace :::"asymmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; theorem :: OPOSET_1:8 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v1_necklace :::"symmetric"::: ) ) & (Bool (Set (Var "O")) "is" ($#v4_orders_2 :::"transitive"::: ) )) "holds" (Bool (Set (Var "O")) "is" ($#v2_oposet_1 :::"SubReFlexive"::: ) )) ; theorem :: OPOSET_1:9 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v3_necklace :::"irreflexive"::: ) ) & (Bool (Set (Var "O")) "is" ($#v4_orders_2 :::"transitive"::: ) )) "holds" (Bool (Set (Var "O")) "is" ($#v2_necklace :::"asymmetric"::: ) )) ; theorem :: OPOSET_1:10 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v2_necklace :::"asymmetric"::: ) )) "holds" (Bool (Set (Var "O")) "is" ($#v3_necklace :::"irreflexive"::: ) )) ; begin definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "O" is :::"SubQuasiOrdered"::: means :: OPOSET_1:def 11 (Bool "(" (Bool "O" "is" ($#v2_oposet_1 :::"SubReFlexive"::: ) ) & (Bool "O" "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ); end; :: deftheorem defines :::"SubQuasiOrdered"::: OPOSET_1:def 11 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v3_oposet_1 :::"SubQuasiOrdered"::: ) ) "iff" (Bool "(" (Bool (Set (Var "O")) "is" ($#v2_oposet_1 :::"SubReFlexive"::: ) ) & (Bool (Set (Var "O")) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ) ")" )); notationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; synonym :::"SubPreOrdered"::: "O" for :::"SubQuasiOrdered"::: ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; attr "O" is :::"QuasiOrdered"::: means :: OPOSET_1:def 12 (Bool "(" (Bool "O" "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool "O" "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ); end; :: deftheorem defines :::"QuasiOrdered"::: OPOSET_1:def 12 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v4_oposet_1 :::"QuasiOrdered"::: ) ) "iff" (Bool "(" (Bool (Set (Var "O")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "O")) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ) ")" )); notationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; synonym :::"PreOrdered"::: "O" for :::"QuasiOrdered"::: ; end; theorem :: OPOSET_1:11 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v4_oposet_1 :::"QuasiOrdered"::: ) )) "holds" (Bool (Set (Var "O")) "is" ($#v3_oposet_1 :::"SubQuasiOrdered"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_oposet_1 :::"QuasiOrdered"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_oposet_1 :::"SubQuasiOrdered"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v3_qmax_1 :::"strict"::: ) ($#v4_oposet_1 :::"QuasiOrdered"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "O" is :::"QuasiPure"::: means :: OPOSET_1:def 13 (Bool "(" (Bool "O" "is" ($#v1_oposet_1 :::"Dneg"::: ) ) & (Bool "O" "is" ($#v4_oposet_1 :::"QuasiOrdered"::: ) ) ")" ); end; :: deftheorem defines :::"QuasiPure"::: OPOSET_1:def 13 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v5_oposet_1 :::"QuasiPure"::: ) ) "iff" (Bool "(" (Bool (Set (Var "O")) "is" ($#v1_oposet_1 :::"Dneg"::: ) ) & (Bool (Set (Var "O")) "is" ($#v4_oposet_1 :::"QuasiOrdered"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_qmax_1 :::"strict"::: ) ($#v1_oposet_1 :::"Dneg"::: ) ($#v4_oposet_1 :::"QuasiOrdered"::: ) ($#v5_oposet_1 :::"QuasiPure"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v3_qmax_1 :::"strict"::: ) ($#v5_oposet_1 :::"QuasiPure"::: ) ; end; definitionmode QuasiPureOrthoRelStr is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_oposet_1 :::"QuasiPure"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "O" is :::"PartialOrdered"::: means :: OPOSET_1:def 14 (Bool "(" (Bool "O" "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool "O" "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool "O" "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ); end; :: deftheorem defines :::"PartialOrdered"::: OPOSET_1:def 14 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v6_oposet_1 :::"PartialOrdered"::: ) ) "iff" (Bool "(" (Bool (Set (Var "O")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "O")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool (Set (Var "O")) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "O" is :::"Pure"::: means :: OPOSET_1:def 15 (Bool "(" (Bool "O" "is" ($#v1_oposet_1 :::"Dneg"::: ) ) & (Bool "O" "is" ($#v6_oposet_1 :::"PartialOrdered"::: ) ) ")" ); end; :: deftheorem defines :::"Pure"::: OPOSET_1:def 15 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v7_oposet_1 :::"Pure"::: ) ) "iff" (Bool "(" (Bool (Set (Var "O")) "is" ($#v1_oposet_1 :::"Dneg"::: ) ) & (Bool (Set (Var "O")) "is" ($#v6_oposet_1 :::"PartialOrdered"::: ) ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_qmax_1 :::"strict"::: ) ($#v1_oposet_1 :::"Dneg"::: ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v7_oposet_1 :::"Pure"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v3_qmax_1 :::"strict"::: ) ($#v7_oposet_1 :::"Pure"::: ) ; end; definitionmode PureOrthoRelStr is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_oposet_1 :::"Pure"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "O" is :::"StrictPartialOrdered"::: means :: OPOSET_1:def 16 (Bool "(" (Bool "O" "is" ($#v2_necklace :::"asymmetric"::: ) ) & (Bool "O" "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ); end; :: deftheorem defines :::"StrictPartialOrdered"::: OPOSET_1:def 16 : (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "O")) "is" ($#v8_oposet_1 :::"StrictPartialOrdered"::: ) ) "iff" (Bool "(" (Bool (Set (Var "O")) "is" ($#v2_necklace :::"asymmetric"::: ) ) & (Bool (Set (Var "O")) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ) ")" )); notationlet "O" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; synonym :::"StrictOrdered"::: "O" for :::"StrictPartialOrdered"::: ; end; theorem :: OPOSET_1:12 (Bool "for" (Set (Var "O")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "st" (Bool (Bool (Set (Var "O")) "is" ($#v8_oposet_1 :::"StrictPartialOrdered"::: ) )) "holds" (Bool (Set (Var "O")) "is" ($#v3_necklace :::"irreflexive"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_oposet_1 :::"StrictPartialOrdered"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_necklace :::"irreflexive"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_oposet_1 :::"StrictPartialOrdered"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_necklace :::"irreflexive"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; registration cluster (Set ($#k2_oposet_1 :::"TrivAsymOrthoRelStr"::: ) ) -> ($#v3_necklace :::"irreflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) ($#v8_oposet_1 :::"StrictPartialOrdered"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_necklace :::"irreflexive"::: ) ($#v3_qmax_1 :::"strict"::: ) ($#v8_oposet_1 :::"StrictPartialOrdered"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; theorem :: OPOSET_1:13 (Bool "for" (Set (Var "QO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_oposet_1 :::"QuasiOrdered"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "st" (Bool (Bool (Set (Var "QO")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Var "QO")) "is" ($#v6_oposet_1 :::"PartialOrdered"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_orders_2 :::"reflexive"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "PO" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "PO"))); attr "f" is :::"Orderinvolutive"::: means :: OPOSET_1:def 17 (Bool "(" (Bool "f" "is" bbbadV1_PARTIT_2()) & (Bool "f" "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" ); end; :: deftheorem defines :::"Orderinvolutive"::: OPOSET_1:def 17 : (Bool "for" (Set (Var "PO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PO"))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" bbbadV1_PARTIT_2()) & (Bool (Set (Var "f")) "is" ($#v5_waybel_0 :::"antitone"::: ) ) ")" ) ")" ))); definitionlet "PO" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "PO" is :::"OrderInvolutive"::: means :: OPOSET_1:def 18 (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "PO") "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ); end; :: deftheorem defines :::"OrderInvolutive"::: OPOSET_1:def 18 : (Bool "for" (Set (Var "PO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "PO")) "is" ($#v10_oposet_1 :::"OrderInvolutive"::: ) ) "iff" (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "PO"))) "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ) ")" )); theorem :: OPOSET_1:14 (Bool (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) )) "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ) ; registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v3_qmax_1 :::"strict"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v7_oposet_1 :::"Pure"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionmode PreOrthoPoset is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v7_oposet_1 :::"Pure"::: ) ($#v10_oposet_1 :::"OrderInvolutive"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionlet "PO" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "PO"))); pred "f" :::"QuasiOrthoComplement_on"::: "PO" means :: OPOSET_1:def 19 (Bool "(" (Bool "f" "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "PO" "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," "PO") & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," "PO") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"QuasiOrthoComplement_on"::: OPOSET_1:def 19 : (Bool "for" (Set (Var "PO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PO"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_oposet_1 :::"QuasiOrthoComplement_on"::: ) (Set (Var "PO"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PO")) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "PO"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "PO"))) ")" ) ")" ) ")" ) ")" ))); definitionlet "PO" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "PO" is :::"QuasiOrthocomplemented"::: means :: OPOSET_1:def 20 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "PO" "," "PO" "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "PO")) & (Bool (Set (Var "f")) ($#r1_oposet_1 :::"QuasiOrthoComplement_on"::: ) "PO") ")" )); end; :: deftheorem defines :::"QuasiOrthocomplemented"::: OPOSET_1:def 20 : (Bool "for" (Set (Var "PO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "PO")) "is" ($#v11_oposet_1 :::"QuasiOrthocomplemented"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "PO")) "," (Set (Var "PO")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "PO")))) & (Bool (Set (Var "f")) ($#r1_oposet_1 :::"QuasiOrthoComplement_on"::: ) (Set (Var "PO"))) ")" )) ")" )); theorem :: OPOSET_1:15 (Bool (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) "is" ($#v11_oposet_1 :::"QuasiOrthocomplemented"::: ) ) ; definitionlet "PO" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "PO"))); pred "f" :::"OrthoComplement_on"::: "PO" means :: OPOSET_1:def 21 (Bool "(" (Bool "f" "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "PO" "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," "PO") & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," "PO") & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," "PO" ")" ) ($#r4_waybel_1 :::"is_maximum_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PO")) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," "PO" ")" ) ($#r3_waybel_1 :::"is_minimum_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "PO")) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"OrthoComplement_on"::: OPOSET_1:def 21 : (Bool "for" (Set (Var "PO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PO"))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_oposet_1 :::"OrthoComplement_on"::: ) (Set (Var "PO"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_oposet_1 :::"Orderinvolutive"::: ) ) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "PO")) "holds" (Bool "(" (Bool ($#r1_yellow_0 :::"ex_sup_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "PO"))) & (Bool ($#r2_yellow_0 :::"ex_inf_of"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "PO"))) & (Bool (Set ($#k1_yellow_0 :::""\/""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "PO")) ")" ) ($#r4_waybel_1 :::"is_maximum_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PO")))) & (Bool (Set ($#k2_yellow_0 :::""/\""::: ) "(" (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "PO")) ")" ) ($#r3_waybel_1 :::"is_minimum_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PO")))) ")" ) ")" ) ")" ) ")" ))); definitionlet "PO" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; attr "PO" is :::"Orthocomplemented"::: means :: OPOSET_1:def 22 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" "PO" "," "PO" "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" "PO")) & (Bool (Set (Var "f")) ($#r2_oposet_1 :::"OrthoComplement_on"::: ) "PO") ")" )); end; :: deftheorem defines :::"Orthocomplemented"::: OPOSET_1:def 22 : (Bool "for" (Set (Var "PO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "PO")) "is" ($#v12_oposet_1 :::"Orthocomplemented"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "PO")) "," (Set (Var "PO")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set "the" ($#u1_robbins1 :::"Compl"::: ) "of" (Set (Var "PO")))) & (Bool (Set (Var "f")) ($#r2_oposet_1 :::"OrthoComplement_on"::: ) (Set (Var "PO"))) ")" )) ")" )); theorem :: OPOSET_1:16 (Bool "for" (Set (Var "PO")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "PO"))) "st" (Bool (Bool (Set (Var "f")) ($#r2_oposet_1 :::"OrthoComplement_on"::: ) (Set (Var "PO")))) "holds" (Bool (Set (Var "f")) ($#r1_oposet_1 :::"QuasiOrthoComplement_on"::: ) (Set (Var "PO"))))) ; theorem :: OPOSET_1:17 (Bool (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) "is" ($#v12_oposet_1 :::"Orthocomplemented"::: ) ) ; registration cluster (Set ($#k1_oposet_1 :::"TrivOrthoRelStr"::: ) ) -> ($#v3_qmax_1 :::"strict"::: ) ($#v11_oposet_1 :::"QuasiOrthocomplemented"::: ) ($#v12_oposet_1 :::"Orthocomplemented"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v11_oposet_1 :::"QuasiOrthocomplemented"::: ) ($#v12_oposet_1 :::"Orthocomplemented"::: ) for ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end; definitionmode QuasiOrthoPoset is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v11_oposet_1 :::"QuasiOrthocomplemented"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; mode OrthoPoset is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_oposet_1 :::"PartialOrdered"::: ) ($#v12_oposet_1 :::"Orthocomplemented"::: ) ($#l2_qmax_1 :::"OrthoRelStr"::: ) ; end;