:: LATSUM_1  semantic presentation begin  
theorem :: LATSUM_1:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "B")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "B"))))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "B")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "B"))))  ")" )) ; 
 definitionlet "R", "S" be    ($#l1_orders_2 :::"RelStr"::: )  ; pred "R" :::"tolerates"::: "S" means :: LATSUM_1:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "S"))  ")" )); end; 





:: deftheorem    defines :::"tolerates"::: LATSUM_1:def 1 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))))  ")" ))  ")" )); 
 begin  definitionlet "R", "S" be    ($#l1_orders_2 :::"RelStr"::: )  ; func "R" :::"[*]"::: "S" ->   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: LATSUM_1:def 2 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "S") ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "R")  ($#k4_relset_1 :::"*"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" "S") ")" )))  ")" ); end; 






:: deftheorem    defines :::"[*]"::: LATSUM_1:def 2 :  (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k2_xboole_0 :::"\/"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#k4_relset_1 :::"*"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))) ")" )))  ")" )  ")" ))); 
 registrationlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "R"  ($#k1_latsum_1 :::"[*]"::: )  "S") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; registrationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "S" be    ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster (Set "R"  ($#k1_latsum_1 :::"[*]"::: )  "S") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )   ; 
end; 
theorem :: LATSUM_1:2 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))  ($#r1_relset_1 :::"c="::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" ))) & (Bool (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S")))  ($#r1_relset_1 :::"c="::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )))  ")" )) ; 
 
theorem :: LATSUM_1:3 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "R")) "is"   ($#v3_orders_2 :::"reflexive"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v3_orders_2 :::"reflexive"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S"))) "is"   ($#v3_orders_2 :::"reflexive"::: )  )) ; 
 begin  
theorem :: LATSUM_1:4 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" ))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Var "R")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R")))))) ; 
 
theorem :: LATSUM_1:5 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" ))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Var "S")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S")))))) ; 
 
theorem :: LATSUM_1:6 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R"))))) "implies" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )))  ")"  &  "("  (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "S"))))) "implies" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )))  ")"   ")" ))) ; 
 
theorem :: LATSUM_1:7 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "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  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )  "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k6_subset_1 :::"\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))  ")" ))) ; 
 
theorem :: LATSUM_1:8 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "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 (Var "R"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Var "R")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b")))  ")" )))) ; 
 
theorem :: LATSUM_1:9 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )  (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Var "S")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b"))) "iff" (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "d")))  ")" )))) ; 
 
theorem :: LATSUM_1:10 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )))) ; 
 
theorem :: LATSUM_1:11 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )))) ; 
 
theorem :: LATSUM_1:12 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))))) ; 
 
theorem :: LATSUM_1:13 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))))) ; 
 
theorem :: LATSUM_1:14 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#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  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "y")))  ")" ))  ")" ))) ; 
 
theorem :: LATSUM_1:15 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "c")) "," (Set (Var "d")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Var "R")) "is"   ($#v4_orders_2 :::"transitive"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b"))) "iff" (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "d")))  ")" )))) ; 
 
theorem :: LATSUM_1:16 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "D")) "being"   ($#v1_waybel_0 :::"directed"::: )     ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))))) ; 
 
theorem :: LATSUM_1:17 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" ))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) "holds"  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) ; 
 
theorem :: LATSUM_1:18 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )  "st" (Bool (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) "holds"  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))))) ; 
 
theorem :: LATSUM_1:19 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#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 (Var "R"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v1_waybel_0 :::"directed"::: )     ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))) & (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "b"))))))) ; 
 
theorem :: LATSUM_1:20 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v1_yellow_0 :::"lower-bounded"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_waybel_0 :::"directed"::: )     ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")))) "holds"  (Bool (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "S")))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) ; 
 
theorem :: LATSUM_1:21 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" ))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))) ; 
 
theorem :: LATSUM_1:22 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" ))) & (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k6_subset_1 :::"\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k6_subset_1 :::"\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))  ")" ))) ; 
 
theorem :: LATSUM_1:23 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S")) ")" )  "st" (Bool (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))) & (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))))) ; 
 
theorem :: LATSUM_1:24 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))) & (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))) & (Bool (Set (Var "R")) "is"   ($#v4_orders_2 :::"transitive"::: )  ) & (Bool (Set (Var "R")) "is"   ($#v5_orders_2 :::"antisymmetric"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v4_orders_2 :::"transitive"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v5_orders_2 :::"antisymmetric"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S"))) "is"   ($#v5_orders_2 :::"antisymmetric"::: )  )) ; 
 
theorem :: LATSUM_1:25 (Bool  "for" (Set (Var "R")) "," (Set (Var "S")) "being"    ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v13_waybel_0 :::"upper"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))) & (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) "is"   ($#v12_waybel_0 :::"lower"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))) & (Bool (Set (Var "R"))  ($#r1_latsum_1 :::"tolerates"::: )  (Set (Var "S"))) & (Bool (Set (Var "R")) "is"   ($#v4_orders_2 :::"transitive"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v4_orders_2 :::"transitive"::: )  )) "holds"  (Bool (Set (Set (Var "R"))  ($#k1_latsum_1 :::"[*]"::: )  (Set (Var "S"))) "is"   ($#v4_orders_2 :::"transitive"::: )  )) ;