:: LATTICE7  semantic presentation begin  definitionlet "L" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "A", "B" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "L")); :: original: :::"c="::: redefine pred "A" :::"c="::: "B" means :: LATTICE7:def 1 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "A")) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "B")); end; 






:: deftheorem    defines :::"c="::: LATTICE7:def 1 :  (Bool  "for" (Set (Var "L")) "being"    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_lattice7 :::"c="::: )  (Set (Var "B"))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))))  ")" ))); 
 registrationlet "L" be   ($#l1_orders_2 :::"LATTICE":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v6_orders_2 :::"strongly_connected"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "L")); 
end; definitionlet "L" be   ($#l1_orders_2 :::"LATTICE":::); let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); assume 
(Bool (Set (Const "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Const "y")))
 ; mode  :::"Chain":::  "of" "x" "," "y" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Chain":::) "of" "L" means :: LATTICE7:def 2 (Bool  "("  (Bool "x"  ($#r2_hidden :::"in"::: )  it) & (Bool "y"  ($#r2_hidden :::"in"::: )  it) & (Bool  "("   "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  it)) "holds"  (Bool  "("  (Bool "x"  ($#r3_orders_2 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Var "z"))  ($#r3_orders_2 :::"<="::: )  "y")  ")" )  ")" )  ")" ); end; 








:: deftheorem    defines :::"Chain"::: LATTICE7:def 2 :  (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "b4")) "is"    ($#m1_lattice7 :::"Chain"::: )   "of" (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) & (Bool  "("   "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "b4")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Var "z"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "y")))  ")" )  ")" )  ")" )  ")" )))); 
 
theorem :: LATTICE7:1 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set  ($#k7_domain_1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k7_domain_1 :::"}"::: ) ) "is"    ($#m1_lattice7 :::"Chain"::: )   "of" (Set (Var "x")) "," (Set (Var "y"))))) ; 
 



definitionlet "L" be   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::); let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); func  :::"height"::: "x" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: LATTICE7:def 3 (Bool  "("  (Bool  "ex" (Set (Var "A")) "being"    ($#m1_lattice7 :::"Chain"::: )   "of" (Set   ($#k3_yellow_0 :::"Bottom"::: )  "L") "," "x" "st" (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A"))))) & (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_lattice7 :::"Chain"::: )   "of" (Set   ($#k3_yellow_0 :::"Bottom"::: )  "L") "," "x" "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  it)  ")" )  ")" ); end; 






:: deftheorem    defines :::"height"::: LATTICE7:def 3 :  (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "x")))) "iff" (Bool  "("  (Bool  "ex" (Set (Var "A")) "being"    ($#m1_lattice7 :::"Chain"::: )   "of" (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "L"))) "," (Set (Var "x")) "st" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A"))))) & (Bool  "("   "for" (Set (Var "A")) "being"    ($#m1_lattice7 :::"Chain"::: )   "of" (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "L"))) "," (Set (Var "x")) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b3")))  ")" )  ")" )  ")" )))); 
 
theorem :: LATTICE7:2 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#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 "a"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "b")))))) ; 
 
theorem :: LATTICE7:3 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "y"))) "iff" (Bool (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: LATTICE7:4 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) "iff" (Bool (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: LATTICE7:5 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: LATTICE7:6 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1)) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "L"))))  ")" ))) ; 
 
theorem :: LATTICE7:7 (Bool  "for" (Set (Var "L")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set   ($#k1_lattice7 :::"height"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)))) ; 
 scheme  :: LATTICE7:sch 1 LattInd{ F1() ->   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "x"))]))
 provided
(Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "b"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "x")))) "holds"  (Bool P1[(Set (Var "b"))])  ")" )) "holds"  (Bool P1[(Set (Var "x"))]))
 proof 


end; begin  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"::: )     ($#v2_waybel_1 :::"distributive"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; definitionlet "L" be   ($#l1_orders_2 :::"LATTICE":::); let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); pred "x" :::"<(1)"::: "y" means :: LATTICE7:def 4 (Bool  "("  (Bool "x"  ($#r2_orders_2 :::"<"::: )  "y") & (Bool  "("   "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "holds"  (Bool  "("   "not" (Bool "x"  ($#r2_orders_2 :::"<"::: )  (Set (Var "z"))) "or"  "not" (Bool (Set (Var "z"))  ($#r2_orders_2 :::"<"::: )  "y")  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"<(1)"::: LATTICE7:def 4 :  (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_lattice7 :::"<(1)"::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "y"))) & (Bool  "("   "for" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "z"))) "or"  "not" (Bool (Set (Var "z"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "y")))  ")" )  ")" )  ")" )  ")" ))); 
 
theorem :: LATTICE7:8 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "not" (Bool (Set (Var "x"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "y"))))  ")" )  ")" )))) ; 
 definitionlet "L" be   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Chain":::) "of" (Set (Const "L")); func  :::"max"::: "A" ->   ($#m1_subset_1 :::"Element":::) "of" "L" means :: LATTICE7:def 5 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "A")) "holds"  (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  it)  ")" ) & (Bool it  ($#r2_hidden :::"in"::: )  "A")  ")" ); end; 






:: deftheorem    defines :::"max"::: LATTICE7:def 5 :  (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Chain":::) "of" (Set (Var "L"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lattice7 :::"max"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "x"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "b3")))  ")" ) & (Bool (Set (Var "b3"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  ")" )))); 
 
theorem :: LATTICE7:9 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "x"))  ($#r2_lattice7 :::"<(1)"::: )  (Set (Var "y")))))) ; 
 definitionlet "L" be   ($#l1_orders_2 :::"LATTICE":::); func  :::"Join-IRR"::: "L" ->   ($#m1_subset_1 :::"Subset":::) "of" "L" equals :: LATTICE7:def 6  "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" "L" : (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_yellow_0 :::"Bottom"::: )  "L")) & (Bool  "("   "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" "L"  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "c")))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" )  ")" )  ")" )  "}"  ; end; 





:: deftheorem    defines :::"Join-IRR"::: LATTICE7:def 6 :  (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::) "holds"  (Bool (Set   ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) : (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "c")))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" )  ")" )  ")" )  "}"  )); 
 
theorem :: LATTICE7:10 (Bool  "for" (Set (Var "L")) "being"   ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_yellow_0 :::"Bottom"::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "c")))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" )  ")" )  ")" )  ")" ))) ; 
 
theorem :: LATTICE7:11 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v2_waybel_1 :::"distributive"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L"))))) "holds"  (Bool  "ex" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "x"))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_orders_2 :::"<"::: )  (Set (Var "x")))) "holds"  (Bool (Set (Var "y"))  ($#r3_orders_2 :::"<="::: )  (Set (Var "z")))  ")" )  ")" )))) ; 
 
theorem :: LATTICE7:12 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v2_waybel_1 :::"distributive"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set   ($#k1_yellow_0 :::"sup"::: )  (Set  "(" (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "x")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 begin  definitionlet "P" be    ($#l1_orders_2 :::"RelStr"::: )  ; func  :::"LOWER"::: "P" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   equals :: LATTICE7:def 7  "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" "P" : (Bool (Set (Var "X")) "is"   ($#v12_waybel_0 :::"lower"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"LOWER"::: LATTICE7:def 7 :  (Bool  "for" (Set (Var "P")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"  (Bool (Set   ($#k4_lattice7 :::"LOWER"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "X")) where X "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "P")) : (Bool (Set (Var "X")) "is"   ($#v12_waybel_0 :::"lower"::: )  )  "}"  )); 
 
theorem :: LATTICE7:13 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v2_waybel_1 :::"distributive"::: )    ($#l1_orders_2 :::"LATTICE":::) (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "L")) "," (Set  "("  ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k4_lattice7 :::"LOWER"::: )  (Set  "("  ($#k5_yellow_0 :::"subrelstr"::: )  (Set  "("  ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L")) ")" ) ")" ) ")" ) ")" ) "st"  (Bool  "("  (Bool (Set (Var "r")) "is"   ($#v23_waybel_0 :::"isomorphic"::: )  ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds"  (Bool (Set (Set (Var "r"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_waybel_0 :::"downarrow"::: )  (Set (Var "a")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L")) ")" )))  ")" )  ")" ))) ; 
 
theorem :: LATTICE7:14 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )     ($#v2_waybel_1 :::"distributive"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"  (Bool (Set (Var "L")) "," (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set  "("  ($#k4_lattice7 :::"LOWER"::: )  (Set  "("  ($#k5_yellow_0 :::"subrelstr"::: )  (Set  "("  ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L")) ")" ) ")" ) ")" ))  ($#r5_waybel_1 :::"are_isomorphic"::: )  )) ; 
 definitionmode  :::"Ring_of_sets":::  ->    ($#m1_hidden :::"set"::: )   means :: LATTICE7:def 8 (Bool it  ($#r1_cohsp_1 :::"includes_lattice_of"::: )  it); end; 




:: deftheorem    defines :::"Ring_of_sets"::: LATTICE7:def 8 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1")) "is"    ($#m2_lattice7 :::"Ring_of_sets"::: )  ) "iff" (Bool (Set (Var "b1"))  ($#r1_cohsp_1 :::"includes_lattice_of"::: )  (Set (Var "b1")))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m2_lattice7 :::"Ring_of_sets"::: )  ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_lattice7 :::"Ring_of_sets"::: )  ; 
cluster (Set   ($#k2_yellow_1 :::"InclPoset"::: )  "X") ->   ($#v2_waybel_1 :::"distributive"::: )     ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )   ; 
end; 
theorem :: LATTICE7:15 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"  (Bool (Set   ($#k4_lattice7 :::"LOWER"::: )  (Set  "("  ($#k5_yellow_0 :::"subrelstr"::: )  (Set  "("  ($#k3_lattice7 :::"Join-IRR"::: )  (Set (Var "L")) ")" ) ")" )) "is"    ($#m2_lattice7 :::"Ring_of_sets"::: )  )) ; 
 
theorem :: LATTICE7:16 (Bool  "for" (Set (Var "L")) "being"   ($#v8_struct_0 :::"finite"::: )    ($#l1_orders_2 :::"LATTICE":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v2_waybel_1 :::"distributive"::: )  ) "iff" (Bool  "ex" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_lattice7 :::"Ring_of_sets"::: )   "st" (Bool (Set (Var "L")) "," (Set   ($#k2_yellow_1 :::"InclPoset"::: )  (Set (Var "X")))  ($#r5_waybel_1 :::"are_isomorphic"::: )  ))  ")" )) ;