:: LFUZZY_0  semantic presentation begin  definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "R" is  :::"real":::  means :: LFUZZY_0:def 1 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#r1_tarski :::"c="::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R"))) "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 (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )  ")" )  ")" ); end; 




:: deftheorem    defines :::"real"::: LFUZZY_0:def 1 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_lfuzzy_0 :::"real"::: )  ) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "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 "R"))))) "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 (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )  ")" )  ")" )  ")" )); 
 definitionlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; attr "R" is  :::"interval":::  means :: LFUZZY_0:def 2 (Bool  "("  (Bool "R" "is"   ($#v1_lfuzzy_0 :::"real"::: )  ) & (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ")" ))  ")" ); end; 




:: deftheorem    defines :::"interval"::: LFUZZY_0:def 2 :  (Bool  "for" (Set (Var "R")) "being"    ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v2_lfuzzy_0 :::"interval"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_lfuzzy_0 :::"real"::: )  ) & (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))  ")" ))  ")" )  ")" )); 
 registration
cluster   ($#v2_lfuzzy_0 :::"interval"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster   ($#v2_struct_0 :::"empty"::: )    ->   ($#v1_lfuzzy_0 :::"real"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: LFUZZY_0:1 (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) (Bool  "ex" (Set (Var "R")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#l1_orders_2 :::"RelStr"::: )   "st"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set (Var "R")) "is"   ($#v1_lfuzzy_0 :::"real"::: )  )  ")" ))) ; 
 registration
cluster   ($#v1_orders_2 :::"strict"::: )     ($#v2_lfuzzy_0 :::"interval"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: LFUZZY_0:2 (Bool  "for" (Set (Var "R1")) "," (Set (Var "R2")) "being"   ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R2"))))) "holds"  (Bool (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R1"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R1"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_orders_2 :::"RelStr"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R2"))) "," (Set  "the"  ($#u1_orders_2 :::"InternalRel"::: )  "of" (Set (Var "R2"))) "#)" ))) ; 
 registrationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; 
cluster   ->   ($#v1_xreal_0 :::"real"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R"); 
end; definitionlet "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"RealPoset"::: "X" ->   ($#v1_orders_2 :::"strict"::: )     ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )   means :: LFUZZY_0:def 3 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  "X"); end; 





:: deftheorem    defines :::"RealPoset"::: LFUZZY_0:def 3 :  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_orders_2 :::"strict"::: )     ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set (Var "X")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" ))); 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k1_lfuzzy_0 :::"RealPoset"::: )  "X") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_orders_2 :::"strict"::: )     ($#v1_lfuzzy_0 :::"real"::: )   ; 
end; notationlet "R" be    ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); synonym "x" :::"<<="::: "y" for "x" :::"<="::: "y"; synonym "y" :::">>="::: "x" for "x" :::"<="::: "y"; antonym "x" :::"~<="::: "y" for "x" :::"<="::: "y"; antonym "y" :::"~>="::: "x" for "x" :::"<="::: "y"; end; 
theorem :: LFUZZY_0:3 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set (Var "x"))  ($#r1_orders_2 :::"<<="::: )  (Set (Var "y")))  ")" ))) ; 
 registration
cluster   ($#v1_lfuzzy_0 :::"real"::: )    ->   ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v16_waybel_0 :::"connected"::: )     ($#v1_lfuzzy_0 :::"real"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); :: original: :::"max"::: redefine func  :::"max":::  "(" "x" "," "y" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "R"; end; definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); :: original: :::"min"::: redefine func  :::"min":::  "(" "x" "," "y" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" "R"; end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lattice3 :::"with_suprema"::: )     ($#v2_lattice3 :::"with_infima"::: )     ($#v1_lfuzzy_0 :::"real"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 











registrationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); 
identify ; 

identify ; 
end; 
theorem :: LFUZZY_0:4 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Set (Var "a"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_lfuzzy_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; 
 
theorem :: LFUZZY_0:5 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Set (Var "a"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_lfuzzy_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; 
 
theorem :: LFUZZY_0:6 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool  "ex" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )  ")" )) "iff" (Bool (Set (Var "R")) "is"   ($#v1_yellow_0 :::"lower-bounded"::: )  )  ")" )) ; 
 
theorem :: LFUZZY_0:7 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lfuzzy_0 :::"real"::: )     ($#l1_orders_2 :::"RelStr"::: )   "holds"   (Bool  "("  (Bool  "ex" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "y")))  ")" )  ")" )) "iff" (Bool (Set (Var "R")) "is"   ($#v2_yellow_0 :::"upper-bounded"::: )  )  ")" )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lfuzzy_0 :::"interval"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_yellow_0 :::"bounded"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; 
theorem :: LFUZZY_0:8 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lfuzzy_0 :::"interval"::: )     ($#l1_orders_2 :::"RelStr"::: )    (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool   ($#r1_yellow_0 :::"ex_sup_of"::: )  (Set (Var "X")) "," (Set (Var "R"))))) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lfuzzy_0 :::"interval"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lattice3 :::"complete"::: )     ($#v2_lfuzzy_0 :::"interval"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_orders_2 :::"reflexive"::: )     ($#v4_orders_2 :::"transitive"::: )     ($#v5_orders_2 :::"antisymmetric"::: )     ($#v16_waybel_0 :::"connected"::: )    ->   ($#v2_waybel_1 :::"distributive"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lfuzzy_0 :::"interval"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v9_waybel_1 :::"Heyting"::: )     ($#v2_lfuzzy_0 :::"interval"::: )    for    ($#l1_orders_2 :::"RelStr"::: )  ; 
end; registration
cluster (Set bbbadK1_XXREAL_1((Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1))) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster (Set   ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )) ->   ($#v1_orders_2 :::"strict"::: )     ($#v1_lfuzzy_0 :::"real"::: )     ($#v2_lfuzzy_0 :::"interval"::: )   ; 
end; begin  
theorem :: LFUZZY_0:9 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"   ($#l1_orders_2 :::"sup-Semilattice":::))  ")" )) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J"))) "is"   ($#v1_lattice3 :::"with_suprema"::: )  ))) ; 
 
theorem :: LFUZZY_0:10 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"   ($#l1_orders_2 :::"Semilattice":::))  ")" )) "holds"  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J"))) "is"   ($#v2_lattice3 :::"with_infima"::: )  ))) ; 
 
theorem :: LFUZZY_0:11 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"   ($#l1_orders_2 :::"Semilattice":::))  ")" )) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k11_lattice3 :::""/\""::: )  (Set (Var "g")) ")" )  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")) ")" )  ($#k11_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "g"))  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")) ")" ))))))) ; 
 
theorem :: LFUZZY_0:12 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"   ($#l1_orders_2 :::"sup-Semilattice":::))  ")" )) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_yellow_1 :::"product"::: )  (Set (Var "J")) ")" )  (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k10_lattice3 :::""\/""::: )  (Set (Var "g")) ")" )  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")) ")" )  ($#k10_lattice3 :::""\/""::: )  (Set  "(" (Set (Var "g"))  ($#k4_waybel_3 :::"."::: )  (Set (Var "i")) ")" ))))))) ; 
 
theorem :: LFUZZY_0:13 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "J")) "being"   ($#v1_yellow_1 :::"RelStr-yielding"::: )     ($#v4_waybel_3 :::"non-Empty"::: )     ($#v5_waybel_3 :::"reflexive-yielding"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "J"))  ($#k3_waybel_3 :::"."::: )  (Set (Var "i"))) "is"   ($#v3_lattice3 :::"complete"::: )     ($#v9_waybel_1 :::"Heyting"::: )    ($#l1_orders_2 :::"LATTICE":::))  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J"))) "is"   ($#v3_lattice3 :::"complete"::: )  ) & (Bool (Set   ($#k5_yellow_1 :::"product"::: )  (Set (Var "J"))) "is"   ($#v9_waybel_1 :::"Heyting"::: )  )  ")" ))) ; 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#v3_lattice3 :::"complete"::: )     ($#v9_waybel_1 :::"Heyting"::: )    ($#l1_orders_2 :::"LATTICE":::); 
cluster (Set "R"  ($#k6_yellow_1 :::"|^"::: )  "A") ->   ($#v9_waybel_1 :::"Heyting"::: )   ; 
end; begin  definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"FuzzyLattice"::: "A" ->   ($#v3_lattice3 :::"complete"::: )     ($#v9_waybel_1 :::"Heyting"::: )    ($#l1_orders_2 :::"LATTICE":::) equals :: LFUZZY_0:def 4 (Set (Set  "("  ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )  ($#k6_yellow_1 :::"|^"::: )  "A"); end; 





:: deftheorem    defines :::"FuzzyLattice"::: LFUZZY_0:def 4 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" )  ($#k6_yellow_1 :::"|^"::: )  (Set (Var "A"))))); 
 
theorem :: LFUZZY_0:14 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "A")) "," (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ))) ; 
 registrationlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  "A") ->   ($#v3_lattice3 :::"complete"::: )     ($#v1_monoid_0 :::"constituted-Functions"::: )     ($#v9_waybel_1 :::"Heyting"::: )   ; 
end; 
theorem :: LFUZZY_0:15 (Bool  "for" (Set (Var "R")) "being"   ($#v3_lattice3 :::"complete"::: )     ($#v9_waybel_1 :::"Heyting"::: )    ($#l1_orders_2 :::"LATTICE":::)  (Bool  "for" (Set (Var "X")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds"  (Bool (Set (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "(" (Set (Var "X")) "," (Set (Var "R")) ")"  ")" )  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set (Var "x"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "y")) ")" ) where x "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) : (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  "}"   "," (Set (Var "R")) ")" ))))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "a" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Const "X")) ")" ); func  :::"@"::: "a" ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "X" equals :: LFUZZY_0:def 5 "a"; end; 






:: deftheorem    defines :::"@"::: LFUZZY_0:def 5 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Var "X")) ")" ) "holds"  (Bool (Set   ($#k5_lfuzzy_0 :::"@"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))); 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "X")); func  "(" "X" "," "f" ")"  :::"@":::  ->   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  "X" ")" ) equals :: LFUZZY_0:def 6 "f"; end; 






:: deftheorem    defines :::"@"::: LFUZZY_0:def 6 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "X")) "holds"  (Bool (Set  "(" (Set (Var "X")) "," (Set (Var "f")) ")"   ($#k6_lfuzzy_0 :::"@"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "f"))))); 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "X")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "x" ->   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ); end; definitionlet "X", "Y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); let "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "Y")); :: original: :::"."::: redefine func "f" :::".":::  "(" "x" "," "y" ")"  ->   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ); end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Const "X")) ")" ); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "x" ->   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ); end; 














theorem :: LFUZZY_0:16 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_lfuzzy_0 :::"."::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "g"))  ($#k7_lfuzzy_0 :::"."::: )  (Set (Var "c"))))  ")" ) "iff" (Bool (Set  "(" (Set (Var "C")) "," (Set (Var "f")) ")"   ($#k6_lfuzzy_0 :::"@"::: )  )  ($#r1_orders_2 :::"<<="::: )  (Set  "(" (Set (Var "C")) "," (Set (Var "g")) ")"   ($#k6_lfuzzy_0 :::"@"::: )  ))  ")" ))) ; 
 
theorem :: LFUZZY_0:17 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Var "C")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "s"))  ($#r1_orders_2 :::"<<="::: )  (Set (Var "t"))) "iff" (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set  "("  ($#k5_lfuzzy_0 :::"@"::: )  (Set (Var "s")) ")" )  ($#k7_lfuzzy_0 :::"."::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k5_lfuzzy_0 :::"@"::: )  (Set (Var "t")) ")" )  ($#k7_lfuzzy_0 :::"."::: )  (Set (Var "c")))))  ")" ))) ; 
 
theorem :: LFUZZY_0:18 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  "(" (Set (Var "C")) "," (Set (Var "f")) ")"   ($#k6_lfuzzy_0 :::"@"::: )  ")" )  ($#k13_lattice3 :::""\/""::: )  (Set  "("  "(" (Set (Var "C")) "," (Set (Var "g")) ")"   ($#k6_lfuzzy_0 :::"@"::: )  ")" ))))) ; 
 
theorem :: LFUZZY_0:19 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Var "C")) ")" ) "holds"  (Bool (Set (Set (Var "s"))  ($#k13_lattice3 :::""\/""::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k5_lfuzzy_0 :::"@"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k5_lfuzzy_0 :::"@"::: )  (Set (Var "t")) ")" ) ")" )))) ; 
 
theorem :: LFUZZY_0:20 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  "(" (Set (Var "C")) "," (Set (Var "f")) ")"   ($#k6_lfuzzy_0 :::"@"::: )  ")" )  ($#k12_lattice3 :::""/\""::: )  (Set  "("  "(" (Set (Var "C")) "," (Set (Var "g")) ")"   ($#k6_lfuzzy_0 :::"@"::: )  ")" ))))) ; 
 
theorem :: LFUZZY_0:21 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k4_lfuzzy_0 :::"FuzzyLattice"::: )  (Set (Var "C")) ")" ) "holds"  (Bool (Set (Set (Var "s"))  ($#k12_lattice3 :::""/\""::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k5_lfuzzy_0 :::"@"::: )  (Set (Var "s")) ")" ) "," (Set  "("  ($#k5_lfuzzy_0 :::"@"::: )  (Set (Var "t")) ")" ) ")" )))) ; 
 begin  scheme  :: LFUZZY_0:sch 1 SupDistributivity{ F1() ->   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::), F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool P2[(Set (Var "y"))])  "}"   "," (Set F1 "("  ")" ) ")"  ")" ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"   "," (Set F1 "("  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ), y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool  "("  (Bool P1[(Set (Var "x"))]) & (Bool P2[(Set (Var "y"))])  ")" )  "}"   "," (Set F1 "("  ")" ) ")" ))
 proof 


end; scheme  :: LFUZZY_0:sch 2 SupDistributivity9{ F1() ->   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::), F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"   "," (Set F1 "("  ")" ) ")"  ")" ) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool P2[(Set (Var "y"))])  "}"   "," (Set F1 "("  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ), y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool  "("  (Bool P1[(Set (Var "x"))]) & (Bool P2[(Set (Var "y"))])  ")" )  "}"   "," (Set F1 "("  ")" ) ")" ))
 proof 


end; scheme  :: LFUZZY_0:sch 3 FraenkelF9R9{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F3 "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) where u1 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), v1 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "u1")) "," (Set (Var "v1"))])  "}"    ($#r1_hidden :::"="::: )   "{"  (Set F4 "(" (Set (Var "u2")) "," (Set (Var "v2")) ")" ) where u2 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), v2 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "u2")) "," (Set (Var "v2"))])  "}"  )
 provided
(Bool  "for" (Set (Var "u")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "u")) "," (Set (Var "v"))])) "holds"  (Bool (Set F3 "(" (Set (Var "u")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "u")) "," (Set (Var "v")) ")" ))))
 proof 


end; scheme  :: LFUZZY_0:sch 4 FraenkelF699R{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "{"  (Set F3 "(" (Set (Var "u1")) "," (Set (Var "v1")) ")" ) where u1 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), v1 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "u1")) "," (Set (Var "v1"))])  "}"    ($#r1_hidden :::"="::: )   "{"  (Set F4 "(" (Set (Var "u2")) "," (Set (Var "v2")) ")" ) where u2 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), v2 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P2[(Set (Var "u2")) "," (Set (Var "v2"))])  "}"  )
 provided
(Bool  "for" (Set (Var "u")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "holds"   (Bool  "("  (Bool P1[(Set (Var "u")) "," (Set (Var "v"))]) "iff" (Bool P2[(Set (Var "u")) "," (Set (Var "v"))])  ")" )))
 and  
(Bool  "for" (Set (Var "u")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "u")) "," (Set (Var "v"))])) "holds"  (Bool (Set F3 "(" (Set (Var "u")) "," (Set (Var "v")) ")" )  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "u")) "," (Set (Var "v")) ")" ))))
 proof 


end; scheme  :: LFUZZY_0:sch 5 SupCommutativity{ F1() ->   ($#v3_lattice3 :::"complete"::: )    ($#l1_orders_2 :::"LATTICE":::), F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ), F5(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool P2[(Set (Var "y"))])  "}"   "," (Set F1 "("  ")" ) ")"  ")" ) where x "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "x"))])  "}"   "," (Set F1 "("  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "("  ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set F5 "(" (Set (Var "x9")) "," (Set (Var "y9")) ")" ) where x9 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) : (Bool P1[(Set (Var "x9"))])  "}"   "," (Set F1 "("  ")" ) ")"  ")" ) where y9 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" ) : (Bool P2[(Set (Var "y9"))])  "}"   "," (Set F1 "("  ")" ) ")" ))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F3 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "x"))]) & (Bool P2[(Set (Var "y"))])) "holds"  (Bool (Set F4 "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))))
 proof 


end; 
theorem :: LFUZZY_0:22 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "Z")) "holds"  (Bool (Set (Set  "(" (Set (Var "R"))  ($#k4_fuzzy_4 :::"(#)"::: )  (Set (Var "S")) ")" )  ($#k8_lfuzzy_0 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "z")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_yellow_0 :::""\/""::: )   "("  "{"  (Set  "(" (Set  "(" (Set (Var "R"))  ($#k8_lfuzzy_0 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )  ($#k12_lattice3 :::""/\""::: )  (Set  "(" (Set (Var "S"))  ($#k8_lfuzzy_0 :::"."::: )   "(" (Set (Var "y")) "," (Set (Var "z")) ")"  ")" ) ")" ) where y "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "Y")) : (Bool verum)  "}"   "," (Set  "("  ($#k1_lfuzzy_0 :::"RealPoset"::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ")" ))))))) ; 
 
theorem :: LFUZZY_0:23 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "W")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "Y")) "," (Set (Var "Z"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"RMembership_Func":::) "of" (Set (Var "Z")) "," (Set (Var "W")) "holds"  (Bool (Set (Set  "(" (Set (Var "R"))  ($#k4_fuzzy_4 :::"(#)"::: )  (Set (Var "S")) ")" )  ($#k4_fuzzy_4 :::"(#)"::: )  (Set (Var "T")))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "R"))  ($#k4_fuzzy_4 :::"(#)"::: )  (Set  "(" (Set (Var "S"))  ($#k4_fuzzy_4 :::"(#)"::: )  (Set (Var "T")) ")" ))))))) ;