:: YELLOW11  semantic presentation begin  



theorem :: YELLOW11:1 (Bool (Num 3)  ($#r1_hidden :::"="::: )  (Set  ($#k8_domain_1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k8_domain_1 :::"}"::: ) )) ; 
 
theorem :: YELLOW11:2 (Bool (Set (Num 2)  ($#k6_subset_1 :::"\"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) ; 
 
theorem :: YELLOW11:3 (Bool (Set (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k7_domain_1 :::"{"::: ) (Num 1) "," (Num 2) ($#k7_domain_1 :::"}"::: ) )) ; 
 
theorem :: YELLOW11:4 (Bool (Set (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Num 2) ($#k6_domain_1 :::"}"::: ) )) ; 
 begin  
theorem :: YELLOW11:5 (Bool  "for" (Set (Var "L")) "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 "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "iff" (Bool (Set (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ))) ; 
 
theorem :: YELLOW11:6 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "b")) ")" )  ($#k13_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")) ")" ))  ($#r3_orders_2 :::"<="::: )  (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "b"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: YELLOW11:7 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "b"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")) ")" ))  ($#r3_orders_2 :::"<="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "b")) ")" )  ($#k12_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "c")) ")" ))))) ; 
 
theorem :: YELLOW11:8 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "b"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")) ")" ))  ($#r3_orders_2 :::"<="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "b")) ")" )  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")))))) ; 
 definitionfunc  :::"N_5":::  ->    ($#l1_orders_2 :::"RelStr"::: )   equals :: YELLOW11:def 1 (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 1) ")" ) "," (Num 2) "," (Set  "(" (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 2) ")" ) "," (Num 3) ($#k3_enumset1 :::"}"::: ) )); end; 




:: deftheorem    defines :::"N_5"::: YELLOW11:def 1 :  (Bool (Set   ($#k1_yellow11 :::"N_5"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  "(" (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 1) ")" ) "," (Num 2) "," (Set  "(" (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 2) ")" ) "," (Num 3) ($#k3_enumset1 :::"}"::: ) ))); 
 registration
cluster (Set   ($#k1_yellow11 :::"N_5"::: )  ) ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 

cluster (Set   ($#k1_yellow11 :::"N_5"::: )  ) ->   ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )   ; 
end; definitionfunc  :::"M_3":::  ->    ($#l1_orders_2 :::"RelStr"::: )   equals :: YELLOW11:def 2 (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set  "(" (Num 2)  ($#k6_subset_1 :::"\"::: )  (Num 1) ")" ) "," (Set  "(" (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 2) ")" ) "," (Num 3) ($#k3_enumset1 :::"}"::: ) )); end; 




:: deftheorem    defines :::"M_3"::: YELLOW11:def 2 :  (Bool (Set   ($#k2_yellow11 :::"M_3"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set  "(" (Num 2)  ($#k6_subset_1 :::"\"::: )  (Num 1) ")" ) "," (Set  "(" (Num 3)  ($#k6_subset_1 :::"\"::: )  (Num 2) ")" ) "," (Num 3) ($#k3_enumset1 :::"}"::: ) ))); 
 registration
cluster (Set   ($#k2_yellow11 :::"M_3"::: )  ) ->   ($#v1_orders_2 :::"strict"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )   ; 

cluster (Set   ($#k2_yellow11 :::"M_3"::: )  ) ->   ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )   ; 
end; 
theorem :: YELLOW11:9 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::) "holds"   (Bool  "("  (Bool  "ex" (Set (Var "K")) "being"   ($#v4_yellow_0 :::"full"::: )    ($#m1_yellow_0 :::"Sublattice":::) "of" (Set (Var "L")) "st" (Bool (Set   ($#k1_yellow11 :::"N_5"::: )  ) "," (Set (Var "K"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "c"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "d"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Set (Var "b"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "b"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set (Var "c"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "b"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "e"))) & (Bool (Set (Set (Var "c"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "e")))  ")" ))  ")" )) ; 
 
theorem :: YELLOW11:10 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::) "holds"   (Bool  "("  (Bool  "ex" (Set (Var "K")) "being"   ($#v4_yellow_0 :::"full"::: )    ($#m1_yellow_0 :::"Sublattice":::) "of" (Set (Var "L")) "st" (Bool (Set   ($#k2_yellow11 :::"M_3"::: )  ) "," (Set (Var "K"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "d"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"<>"::: )  (Set (Var "e"))) & (Bool (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "b"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set (Var "c"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Set (Var "d"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "d"))) & (Bool (Set (Set (Var "b"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "b"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "c"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "b"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "e"))) & (Bool (Set (Set (Var "b"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "e"))) & (Bool (Set (Set (Var "c"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Var "e")))  ")" ))  ")" )) ; 
 begin  definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; attr "L" is  :::"modular":::  means :: YELLOW11:def 3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k10_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "b"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "b")) ")" )  ($#k11_lattice3 :::""/\""::: )  (Set (Var "c"))))); end; 




:: deftheorem    defines :::"modular"::: YELLOW11:def 3 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v1_yellow11 :::"modular"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "a"))  ($#k10_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "b"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "b")) ")" )  ($#k11_lattice3 :::""/\""::: )  (Set (Var "c")))))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#v2_waybel_1 :::"distributive"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#v1_yellow11 :::"modular"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: YELLOW11:11 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v1_yellow11 :::"modular"::: )  ) "iff" (Bool  "for" (Set (Var "K")) "being"   ($#v4_yellow_0 :::"full"::: )    ($#m1_yellow_0 :::"Sublattice":::) "of" (Set (Var "L"))  "holds" (Bool (Bool  "not" (Set   ($#k1_yellow11 :::"N_5"::: )  ) "," (Set (Var "K"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )))  ")" )) ; 
 
theorem :: YELLOW11:12 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  "st" (Bool (Bool (Set (Var "L")) "is"   ($#v1_yellow11 :::"modular"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v2_waybel_1 :::"distributive"::: )  ) "iff" (Bool  "for" (Set (Var "K")) "being"   ($#v4_yellow_0 :::"full"::: )    ($#m1_yellow_0 :::"Sublattice":::) "of" (Set (Var "L"))  "holds" (Bool (Bool  "not" (Set   ($#k2_yellow11 :::"M_3"::: )  ) "," (Set (Var "K"))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )))  ")" )) ; 
 begin  definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func :::"[#":::"a" "," "b":::"#]"::: ->   ($#m1_subset_1 :::"Subset":::) "of" "L" means :: YELLOW11:def 4 (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L" "holds"   (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool "a"  ($#r1_orders_2 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  "b")  ")" )  ")" )); end; 







:: deftheorem    defines :::"[#"::: YELLOW11:def 4 :  (Bool  "for" (Set (Var "L")) "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 "L"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_yellow11 :::"[#"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_yellow11 :::"#]"::: ) )) "iff" (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_orders_2 :::"<="::: )  (Set (Var "b")))  ")" )  ")" ))  ")" )))); 
 definitionlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "IT" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); attr "IT" is  :::"interval":::  means :: YELLOW11:def 5 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L" "st" (Bool "IT"  ($#r1_hidden :::"="::: )  (Set  ($#k3_yellow11 :::"[#"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_yellow11 :::"#]"::: ) ))); end; 





:: deftheorem    defines :::"interval"::: YELLOW11:def 5 :  (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_yellow11 :::"interval"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_yellow11 :::"[#"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_yellow11 :::"#]"::: ) )))  ")" ))); 
 registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_yellow11 :::"interval"::: )    ->   ($#v1_waybel_0 :::"directed"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L"))); 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_yellow11 :::"interval"::: )    ->   ($#v2_waybel_0 :::"filtered"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L"))); 
end; registrationlet "L" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_orders_2 :::"RelStr"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); 
cluster (Set  ($#k3_yellow11 :::"[#"::: ) "a" "," "b" ($#k3_yellow11 :::"#]"::: ) ) ->   ($#v2_yellow11 :::"interval"::: )   ; 
end; 
theorem :: YELLOW11:13 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set  ($#k3_yellow11 :::"[#"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_yellow11 :::"#]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_waybel_0 :::"uparrow"::: )  (Set (Var "a")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "b")) ")" ))))) ; 
 registrationlet "L" be   ($#v2_lattice3 :::"with_infima"::: )    ($#l1_orders_2 :::"Poset":::); let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); 
cluster (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set  ($#k3_yellow11 :::"[#"::: ) "a" "," "b" ($#k3_yellow11 :::"#]"::: ) )) ->   ($#v5_yellow_0 :::"meet-inheriting"::: )   ; 
end; registrationlet "L" be   ($#v1_lattice3 :::"with_suprema"::: )    ($#l1_orders_2 :::"Poset":::); let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); 
cluster (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set  ($#k3_yellow11 :::"[#"::: ) "a" "," "b" ($#k3_yellow11 :::"#]"::: ) )) ->   ($#v6_yellow_0 :::"join-inheriting"::: )   ; 
end; 
theorem :: YELLOW11:14 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "L")) "is"   ($#v1_yellow11 :::"modular"::: )  )) "holds"  (Bool (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set  ($#k3_yellow11 :::"[#"::: ) (Set (Var "b")) "," (Set  "(" (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "b")) ")" ) ($#k3_yellow11 :::"#]"::: ) )) "," (Set   ($#k5_yellow_0 :::"subrelstr"::: )  (Set  ($#k3_yellow11 :::"[#"::: ) (Set  "(" (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "b")) ")" ) "," (Set (Var "a")) ($#k3_yellow11 :::"#]"::: ) ))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ))) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )   bbbadV2_ORDERS_2()   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster   ($#v8_struct_0 :::"finite"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v2_lattice3 :::"with_infima"::: )    ->   ($#v1_yellow_0 :::"lower-bounded"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster   ($#v8_struct_0 :::"finite"::: )     ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )    ->   ($#v3_lattice3 :::"complete"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end;