:: YELLOW10  semantic presentation begin  registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_yellow_0 :::"upper-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v2_yellow_0 :::"upper-bounded"::: )   ; 
end; registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_yellow_0 :::"lower-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v1_yellow_0 :::"lower-bounded"::: )   ; 
end; 
theorem :: YELLOW10:1 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v2_yellow_0 :::"upper-bounded"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_yellow_0 :::"upper-bounded"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v2_yellow_0 :::"upper-bounded"::: )  )  ")" )) ; 
 
theorem :: YELLOW10:2 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  )  ")" )) ; 
 
theorem :: YELLOW10:3 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_yellow_0 :::"upper-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k4_yellow_0 :::"Top"::: )  (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set  "("  ($#k4_yellow_0 :::"Top"::: )  (Set (Var "S")) ")" ) "," (Set  "("  ($#k4_yellow_0 :::"Top"::: )  (Set (Var "T")) ")" ) ($#k7_yellow_3 :::"]"::: ) ))) ; 
 
theorem :: YELLOW10:4 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_yellow_0 :::"lower-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set  "("  ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "S")) ")" ) "," (Set  "("  ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "T")) ")" ) ($#k7_yellow_3 :::"]"::: ) ))) ; 
 
theorem :: YELLOW10:5 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_yellow_0 :::"lower-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool  "("  (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v3_lattice3 :::"complete"::: )  ) "or" (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "D")) "," (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ))  ")" )) "holds"  (Bool (Set   ($#k1_yellow_0 :::"sup"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set  "("  ($#k1_yellow_0 :::"sup"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "D")) ")" ) ")" ) "," (Set  "("  ($#k1_yellow_0 :::"sup"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "D")) ")" ) ")" ) ($#k7_yellow_3 :::"]"::: ) )))) ; 
 
theorem :: YELLOW10:6 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_yellow_0 :::"upper-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool  "("  (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v3_lattice3 :::"complete"::: )  ) "or" (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set (Var "D")) "," (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ))  ")" )) "holds"  (Bool (Set   ($#k2_yellow_0 :::"inf"::: )  (Set (Var "D")))  ($#r1_hidden :::"="::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set  "("  ($#k2_yellow_0 :::"inf"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "D")) ")" ) ")" ) "," (Set  "("  ($#k2_yellow_0 :::"inf"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "D")) ")" ) ")" ) ($#k7_yellow_3 :::"]"::: ) )))) ; 
 
theorem :: YELLOW10:7 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) "iff" (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  )  ($#r1_lattice3 :::"is_<=_than"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  )  ($#r1_lattice3 :::"is_<=_than"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) ($#k6_domain_1 :::"}"::: ) ))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:8 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_lattice3 :::"is_<=_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k7_domain_1 :::"}"::: ) )) "iff" (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  )  ($#r1_lattice3 :::"is_<=_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) "," (Set  "(" (Set (Var "z"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  )  ($#r1_lattice3 :::"is_<=_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) "," (Set  "(" (Set (Var "z"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) ))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:9 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_lattice3 :::"is_>=_than"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )) "iff" (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  )  ($#r2_lattice3 :::"is_>=_than"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  )  ($#r2_lattice3 :::"is_>=_than"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) ($#k6_domain_1 :::"}"::: ) ))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:10 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_lattice3 :::"is_>=_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k7_domain_1 :::"}"::: ) )) "iff" (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  )  ($#r2_lattice3 :::"is_>=_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) "," (Set  "(" (Set (Var "z"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  )  ($#r2_lattice3 :::"is_>=_than"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) "," (Set  "(" (Set (Var "z"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) ))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:11 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )) "iff" (Bool  "("  (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) "," (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "S"))) & (Bool   ($#r2_yellow_0 :::"ex_inf_of"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) "," (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "T")))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:12 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "," (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )) "iff" (Bool  "("  (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) "," (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "S"))) & (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) "," (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" ) ($#k7_domain_1 :::"}"::: ) ) "," (Set (Var "T")))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:13 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y")) ")" )  ($#k8_yellow_3 :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" )  ($#k12_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y")) ")" )  ($#k9_yellow_3 :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )  ($#k12_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:14 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y")) ")" )  ($#k8_yellow_3 :::"`1"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" )  ($#k13_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  ")" ))) & (Bool (Set (Set  "(" (Set (Var "x"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y")) ")" )  ($#k9_yellow_3 :::"`2"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )  ($#k13_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:15 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "x2")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k7_yellow_3 :::"["::: ) (Set  "(" (Set (Var "x1"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y1")) ")" ) "," (Set  "(" (Set (Var "x2"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y2")) ")" ) ($#k7_yellow_3 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k7_yellow_3 :::"]"::: ) )  ($#k12_lattice3 :::""/\""::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k7_yellow_3 :::"]"::: ) )))))) ; 
 
theorem :: YELLOW10:16 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "x2")) "," (Set (Var "y2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k7_yellow_3 :::"["::: ) (Set  "(" (Set (Var "x1"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y1")) ")" ) "," (Set  "(" (Set (Var "x2"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y2")) ")" ) ($#k7_yellow_3 :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k7_yellow_3 :::"]"::: ) )  ($#k13_lattice3 :::""\/""::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k7_yellow_3 :::"]"::: ) )))))) ; 
 definitionlet "S" be   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); :: original: :::"is_a_complement_of"::: redefine pred "y" :::"is_a_complement_of"::: "x"; symmetry  
(Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S"))  "st" (Bool (Bool bbbadR6_WAYBEL_1((Set (Const "S")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) "holds"  (Bool bbbadR6_WAYBEL_1((Set (Const "S")) "," (Set (Var "b1")) "," (Set (Var "b2")))))
 ; end; 
theorem :: YELLOW10:17 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v3_yellow_0 :::"bounded"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_yellow10 :::"is_a_complement_of"::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  )  ($#r1_yellow10 :::"is_a_complement_of"::: )  (Set (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  )  ($#r1_yellow10 :::"is_a_complement_of"::: )  (Set (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:18 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_yellow_3 :::"]"::: ) )  ($#r1_waybel_3 :::"<<"::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k7_yellow_3 :::"]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_waybel_3 :::"<<"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_waybel_3 :::"<<"::: )  (Set (Var "d")))  ")" )))) ; 
 
theorem :: YELLOW10:19 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "b")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_yellow_3 :::"]"::: ) )  ($#r1_waybel_3 :::"<<"::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k7_yellow_3 :::"]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_waybel_3 :::"<<"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_waybel_3 :::"<<"::: )  (Set (Var "d")))  ")" )  ")" )))) ; 
 
theorem :: YELLOW10:20 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_waybel_3 :::"<<"::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  )  ($#r1_waybel_3 :::"<<"::: )  (Set (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  )  ($#r1_waybel_3 :::"<<"::: )  (Set (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ))  ")" ))) ; 
 
theorem :: YELLOW10:21 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_waybel_3 :::"<<"::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  )  ($#r1_waybel_3 :::"<<"::: )  (Set (Set (Var "y"))  ($#k8_yellow_3 :::"`1"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  )  ($#r1_waybel_3 :::"<<"::: )  (Set (Set (Var "y"))  ($#k9_yellow_3 :::"`2"::: )  ))  ")" )  ")" ))) ; 
 
theorem :: YELLOW10:22 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "x")) "is"   ($#v1_waybel_3 :::"compact"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ) "is"   ($#v1_waybel_3 :::"compact"::: )  ) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ) "is"   ($#v1_waybel_3 :::"compact"::: )  )  ")" ))) ; 
 
theorem :: YELLOW10:23 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ) "is"   ($#v1_waybel_3 :::"compact"::: )  ) & (Bool (Set (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ) "is"   ($#v1_waybel_3 :::"compact"::: )  )) "holds"  (Bool (Set (Var "x")) "is"   ($#v1_waybel_3 :::"compact"::: )  ))) ; 
 begin  
theorem :: YELLOW10:24 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "(" (Set (Var "X"))  ($#k4_yellow_4 :::""/\""::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" )  ($#k4_yellow_4 :::""/\""::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "Y")) ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "(" (Set (Var "X"))  ($#k4_yellow_4 :::""/\""::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" )  ($#k4_yellow_4 :::""/\""::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "Y")) ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:25 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "(" (Set (Var "X"))  ($#k2_yellow_4 :::""\/""::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" )  ($#k2_yellow_4 :::""\/""::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "Y")) ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "(" (Set (Var "X"))  ($#k2_yellow_4 :::""\/""::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" )  ($#k2_yellow_4 :::""\/""::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "Y")) ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:26 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" ) ")" ) "," (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" ) ")" ) ($#k6_yellow_3 :::":]"::: ) )))) ; 
 
theorem :: YELLOW10:27 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "Y")) ")" ) ($#k6_yellow_3 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  ($#k6_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_yellow_3 :::":]"::: ) )))))) ; 
 
theorem :: YELLOW10:28 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:29 (Bool  "for" (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" )))))) ; 
 
theorem :: YELLOW10:30 (Bool  "for" (Set (Var "S")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k3_waybel_0 :::"downarrow"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_waybel_0 :::"downarrow"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" )))))) ; 
 
theorem :: YELLOW10:31 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" ) ")" ) "," (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" ) ")" ) ($#k6_yellow_3 :::":]"::: ) )))) ; 
 
theorem :: YELLOW10:32 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "Y")) ")" ) ($#k6_yellow_3 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set  ($#k6_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_yellow_3 :::":]"::: ) )))))) ; 
 
theorem :: YELLOW10:33 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "X")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "X")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:34 (Bool  "for" (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set  "("  ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X")) ")" )))))) ; 
 
theorem :: YELLOW10:35 (Bool  "for" (Set (Var "S")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k4_waybel_0 :::"uparrow"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_waybel_0 :::"uparrow"::: )  (Set  "("  ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X")) ")" )))))) ; 
 
theorem :: YELLOW10:36 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "t")) ")" ) ($#k6_yellow_3 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k7_yellow_3 :::"]"::: ) )))))) ; 
 
theorem :: YELLOW10:37 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:38 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" )))))) ; 
 
theorem :: YELLOW10:39 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_waybel_0 :::"downarrow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))))) ; 
 
theorem :: YELLOW10:40 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  "("  ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "t")) ")" ) ($#k6_yellow_3 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_waybel_0 :::"uparrow"::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k7_yellow_3 :::"]"::: ) )))))) ; 
 
theorem :: YELLOW10:41 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_waybel_0 :::"uparrow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_waybel_0 :::"uparrow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:42 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_waybel_0 :::"uparrow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" )))))) ; 
 
theorem :: YELLOW10:43 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_waybel_0 :::"uparrow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))))) ; 
 
theorem :: YELLOW10:44 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k13_yellow_3 :::"[:"::: ) (Set  "("  ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "t")) ")" ) ($#k13_yellow_3 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_waybel_3 :::"waybelow"::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k7_yellow_3 :::"]"::: ) )))))) ; 
 
theorem :: YELLOW10:45 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_waybel_3 :::"waybelow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_waybel_3 :::"waybelow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:46 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_waybel_3 :::"waybelow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" )))))) ; 
 
theorem :: YELLOW10:47 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k1_waybel_3 :::"waybelow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_waybel_3 :::"waybelow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))))) ; 
 
theorem :: YELLOW10:48 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k12_yellow_3 :::"[:"::: ) (Set  "("  ($#k2_waybel_3 :::"wayabove"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k2_waybel_3 :::"wayabove"::: )  (Set (Var "t")) ")" ) ($#k12_yellow_3 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_3 :::"wayabove"::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k7_yellow_3 :::"]"::: ) )))))) ; 
 
theorem :: YELLOW10:49 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k2_waybel_3 :::"wayabove"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_waybel_3 :::"wayabove"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k2_waybel_3 :::"wayabove"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_waybel_3 :::"wayabove"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:50 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set  "("  ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "t")) ")" ) ($#k6_yellow_3 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set  ($#k7_yellow_3 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k7_yellow_3 :::"]"::: ) )))))) ; 
 
theorem :: YELLOW10:51 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" ))) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))  ")" ))) ; 
 
theorem :: YELLOW10:52 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set  "("  ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set  "(" (Set (Var "x"))  ($#k8_yellow_3 :::"`1"::: )  ")" )))))) ; 
 
theorem :: YELLOW10:53 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "holds"  (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set  "("  ($#k2_waybel_8 :::"compactbelow"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel_8 :::"compactbelow"::: )  (Set  "(" (Set (Var "x"))  ($#k9_yellow_3 :::"`2"::: )  ")" )))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v1_waybel_6 :::"Open"::: )    for  bbbadM1_SUBSET_1((Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))); 
end; 
theorem :: YELLOW10:54 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_waybel_6 :::"Open"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X"))) "is"   ($#v1_waybel_6 :::"Open"::: )  ) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X"))) "is"   ($#v1_waybel_6 :::"Open"::: )  )  ")" ))) ; 
 
theorem :: YELLOW10:55 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_waybel_6 :::"Open"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v1_waybel_6 :::"Open"::: )  )) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_yellow_3 :::":]"::: ) ) "is"   ($#v1_waybel_6 :::"Open"::: )  )))) ; 
 
theorem :: YELLOW10:56 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_waybel11 :::"inaccessible"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X"))) "is"   ($#v1_waybel11 :::"inaccessible"::: )  ) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X"))) "is"   ($#v1_waybel11 :::"inaccessible"::: )  )  ")" ))) ; 
 
theorem :: YELLOW10:57 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_waybel11 :::"inaccessible"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v1_waybel11 :::"inaccessible"::: )  )) "holds"  (Bool (Set  ($#k12_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k12_yellow_3 :::":]"::: ) ) "is"   ($#v1_waybel11 :::"inaccessible"::: )  )))) ; 
 
theorem :: YELLOW10:58 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_yellow_3 :::":]"::: ) ) "is"   ($#v2_waybel11 :::"directly_closed"::: )  )) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set (Var "X")) "is"   ($#v2_waybel11 :::"directly_closed"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool (Set (Var "Y")) "is"   ($#v2_waybel11 :::"directly_closed"::: )  )  ")"   ")" )))) ; 
 
theorem :: YELLOW10:59 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v2_waybel11 :::"directly_closed"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v2_waybel11 :::"directly_closed"::: )  )) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_yellow_3 :::":]"::: ) ) "is"   ($#v2_waybel11 :::"directly_closed"::: )  )))) ; 
 
theorem :: YELLOW10:60 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_waybel11 :::"property(S)"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k4_yellow_3 :::"proj1"::: )  (Set (Var "X"))) "is"   ($#v3_waybel11 :::"property(S)"::: )  ) & (Bool (Set   ($#k5_yellow_3 :::"proj2"::: )  (Set (Var "X"))) "is"   ($#v3_waybel11 :::"property(S)"::: )  )  ")" ))) ; 
 
theorem :: YELLOW10:61 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_waybel11 :::"property(S)"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v3_waybel11 :::"property(S)"::: )  )) "holds"  (Bool (Set  ($#k6_yellow_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_yellow_3 :::":]"::: ) ) "is"   ($#v3_waybel11 :::"property(S)"::: )  )))) ; 
 begin  
theorem :: YELLOW10:62 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "S")) "is"   ($#v25_waybel_0 :::"/\-complete"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v25_waybel_0 :::"/\-complete"::: )  )) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v25_waybel_0 :::"/\-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "S") "#)" ) ->   ($#v25_waybel_0 :::"/\-complete"::: )   ; 
end; registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v25_waybel_0 :::"/\-complete"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v25_waybel_0 :::"/\-complete"::: )   ; 
end; 
theorem :: YELLOW10:63 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v25_waybel_0 :::"/\-complete"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v25_waybel_0 :::"/\-complete"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v25_waybel_0 :::"/\-complete"::: )  )  ")" )) ; 
 registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v3_yellow_0 :::"bounded"::: )     ($#v10_waybel_1 :::"complemented"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v10_waybel_1 :::"complemented"::: )   ; 
end; 
theorem :: YELLOW10:64 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v3_yellow_0 :::"bounded"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v10_waybel_1 :::"complemented"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v10_waybel_1 :::"complemented"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v10_waybel_1 :::"complemented"::: )  )  ")" )) ; 
 registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_waybel_1 :::"distributive"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v2_waybel_1 :::"distributive"::: )   ; 
end; 
theorem :: YELLOW10:65 (Bool  "for" (Set (Var "S")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v2_waybel_1 :::"distributive"::: )  )) "holds"  (Bool (Set (Var "S")) "is"   ($#v2_waybel_1 :::"distributive"::: )  ))) ; 
 
theorem :: YELLOW10:66 (Bool  "for" (Set (Var "S")) "being"   ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "T")) "being"   ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v2_waybel_1 :::"distributive"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v2_waybel_1 :::"distributive"::: )  ))) ; 
 registrationlet "S", "T" be   ($#v2_waybel_2 :::"meet-continuous"::: )    ($#l1_orders_2 :::"Semilattice":::); 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v1_waybel_2 :::"satisfying_MC"::: )   ; 
end; 
theorem :: YELLOW10:67 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_orders_2 :::"Semilattice":::)  "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v2_waybel_2 :::"meet-continuous"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_waybel_2 :::"meet-continuous"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v2_waybel_2 :::"meet-continuous"::: )  )  ")" )) ; 
 registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v24_waybel_0 :::"up-complete"::: )     ($#v25_waybel_0 :::"/\-complete"::: )     ($#v2_waybel_3 :::"satisfying_axiom_of_approximation"::: )    ($#l1_orders_2 :::"Poset":::); 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v2_waybel_3 :::"satisfying_axiom_of_approximation"::: )   ; 
end; registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v25_waybel_0 :::"/\-complete"::: )     ($#v3_waybel_3 :::"continuous"::: )    ($#l1_orders_2 :::"Poset":::); 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v3_waybel_3 :::"continuous"::: )   ; 
end; 
theorem :: YELLOW10:68 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v24_waybel_0 :::"up-complete"::: )    ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v3_waybel_3 :::"continuous"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v3_waybel_3 :::"continuous"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v3_waybel_3 :::"continuous"::: )  )  ")" )) ; 
 registrationlet "S", "T" be   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v24_waybel_0 :::"up-complete"::: )     ($#v1_waybel_8 :::"satisfying_axiom_K"::: )    ($#l1_orders_2 :::"sup-Semilattice":::); 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v1_waybel_8 :::"satisfying_axiom_K"::: )   ; 
end; registrationlet "S", "T" be   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v3_lattice3 :::"complete"::: )     ($#v2_waybel_8 :::"algebraic"::: )    ($#l1_orders_2 :::"sup-Semilattice":::); 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v2_waybel_8 :::"algebraic"::: )   ; 
end; 
theorem :: YELLOW10:69 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"Poset":::)  "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v2_waybel_8 :::"algebraic"::: )  )  ")" )) ; 
 registrationlet "S", "T" be   ($#v1_yellow_0 :::"lower-bounded"::: )     ($#v3_waybel_8 :::"arithmetic"::: )    ($#l1_orders_2 :::"LATTICE":::); 
cluster (Set  ($#k3_yellow_3 :::"[:"::: ) "S" "," "T" ($#k3_yellow_3 :::":]"::: ) ) ->   ($#v3_waybel_8 :::"arithmetic"::: )   ; 
end; 
theorem :: YELLOW10:70 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#v1_yellow_0 :::"lower-bounded"::: )    ($#l1_orders_2 :::"LATTICE":::)  "st" (Bool (Bool (Set  ($#k3_yellow_3 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k3_yellow_3 :::":]"::: ) ) "is"   ($#v3_waybel_8 :::"arithmetic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v3_waybel_8 :::"arithmetic"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v3_waybel_8 :::"arithmetic"::: )  )  ")" )) ;