:: FUZZY_1  semantic presentation begin  











registrationlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set bbbadK4_FUNCT_3("x" "," "y")) -> (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )  ($#v5_relat_1 :::"-valued"::: )   ; 
end; registrationlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   "C"  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )   (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2("C" "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#v2_valued_0 :::"ext-real-valued"::: )     ($#v3_valued_0 :::"real-valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("C" "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; mode Membership_Func of "C" is (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )  ($#v5_relat_1 :::"-valued"::: )    ($#m1_subset_1 :::"Function":::) "of" "C" "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; 
theorem :: FUZZY_1:1 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "C")) "," (Set (Var "C")) ")" ) "is"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")))) ; 
 





registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k1_rcomp_1 :::"[."::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2("X" "," (Set   ($#k1_numbers :::"REAL"::: )  ))  ->   ($#v3_valued_0 :::"real-valued"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; definitionlet "f", "g" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); pred "f" :::"is_less_than"::: "g" means :: FUZZY_1:def 1 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "g")) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f"))) "holds"  (Bool (Set "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set "g"  ($#k1_seq_1 :::"."::: )  (Set (Var "x"))))  ")" )  ")" ); reflexivity  
(Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x"))))  ")" )  ")" ))
 ; end; 





:: deftheorem    defines :::"is_less_than"::: FUZZY_1:def 1 :  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"is_less_than"::: )  (Set (Var "g"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x"))))  ")" )  ")" )  ")" )); 
 notationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f", "g" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "X")); synonym "f" :::"c="::: "g" for "X" :::"is_less_than"::: "f"; end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f", "g" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "X")); :: original: :::"is_less_than"::: redefine pred "f" :::"is_less_than"::: "g" means :: FUZZY_1:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "X" "holds"  (Bool (Set "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set "g"  ($#k1_seq_1 :::"."::: )  (Set (Var "x"))))); end; 






:: deftheorem    defines :::"is_less_than"::: FUZZY_1:def 2 :  (Bool  "for" (Set (Var "X")) "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 "X")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_fuzzy_1 :::"is_less_than"::: )  (Set (Var "g"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))))  ")" ))); 
 
theorem :: FUZZY_1:2 (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 (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set (Var "g"))) "iff" (Bool  "("  (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  )  ")" )  ")" ))) ; 
 
theorem :: FUZZY_1:3 (Bool  "for" (Set (Var "C")) "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 "C")) "holds"  (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:4 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 begin  definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "h", "g" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func  :::"min":::  "(" "h" "," "g" ")"  ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "C" means :: FUZZY_1:def 3 (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "C" "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_square_1 :::"min"::: )   "(" (Set  "(" "h"  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" "g"  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))); idempotence  
(Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_square_1 :::"min"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))))
 ; commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "h")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C"))  "st" (Bool (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_square_1 :::"min"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))  ")" )) "holds"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_square_1 :::"min"::: )   "(" (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))))
 ; end; 







:: deftheorem    defines :::"min"::: FUZZY_1:def 3 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "h")) "," (Set (Var "g")) ")" )) "iff" (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_square_1 :::"min"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" )))  ")" ))); 
 definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "h", "g" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func  :::"max":::  "(" "h" "," "g" ")"  ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "C" means :: FUZZY_1:def 4 (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "C" "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_square_1 :::"max"::: )   "(" (Set  "(" "h"  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" "g"  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))); idempotence  
(Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C"))  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_square_1 :::"max"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))))
 ; commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "h")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C"))  "st" (Bool (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_square_1 :::"max"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))  ")" )) "holds"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_square_1 :::"max"::: )   "(" (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))))
 ; end; 







:: deftheorem    defines :::"max"::: FUZZY_1:def 4 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "h")) "," (Set (Var "g")) ")" )) "iff" (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_square_1 :::"max"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" )))  ")" ))); 
 definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "h" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func  :::"1_minus"::: "h" ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "C" means :: FUZZY_1:def 5 (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "C" "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" "h"  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" )))); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C"))  "st" (Bool (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "C")) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" )))))
 ; end; 






:: deftheorem    defines :::"1_minus"::: FUZZY_1:def 5 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "h")))) "iff" (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ))))  ")" ))); 
 
theorem :: FUZZY_1:5 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "h")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k1_square_1 :::"min"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "h")) "," (Set (Var "g")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))) & (Bool (Set   ($#k2_square_1 :::"max"::: )   "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "h")) "," (Set (Var "g")) ")"  ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "c"))))  ")" )))) ; 
 
theorem :: FUZZY_1:6 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "h")) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "h"))) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "h")) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "h"))) & (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "h")) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "h")) "," (Set (Var "h")) ")" )) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "f")) ")" )) & (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "f")) ")" ))  ")" ))) ; 
 
theorem :: FUZZY_1:7 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")"  ")" ) ")" )) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")"  ")" ) ")" ))  ")" ))) ; 
 
theorem :: FUZZY_1:8 (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 (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f")))  ")" ))) ; 
 
theorem :: FUZZY_1:9 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")"  ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" ) ")" )) & (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")"  ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" ) ")" ))  ")" ))) ; 
 
theorem :: FUZZY_1:10 canceled; 
 
theorem :: FUZZY_1:11 (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 (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "g")) ")" ) ")" )) & (Bool (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "f")) ")" ) "," (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "g")) ")" ) ")" ))  ")" ))) ; 
 begin  
theorem :: FUZZY_1:12 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "C")) ")" ) "is"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")))) ; 
 definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"EMF"::: "C" ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "C" equals :: FUZZY_1:def 6 (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," "C" ")" ); end; 





:: deftheorem    defines :::"EMF"::: FUZZY_1:def 6 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "C")) ")" ))); 
 definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"UMF"::: "C" ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "C" equals :: FUZZY_1:def 7 (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" "C" "," "C" ")" ); end; 





:: deftheorem    defines :::"UMF"::: FUZZY_1:def 7 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "C")) "," (Set (Var "C")) ")" ))); 
 
theorem :: FUZZY_1:13 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))  ")" ))))) ; 
 
theorem :: FUZZY_1:14 (Bool  "for" (Set (Var "C")) "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 "C")) "holds"  (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:15 (Bool  "for" (Set (Var "C")) "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 "C")) "holds"  (Bool (Set   ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:16 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C"))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "x"))))  ")" )))) ; 
 
theorem :: FUZZY_1:17 (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 (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  )  ")" ))) ; 
 
theorem :: FUZZY_1:18 (Bool  "for" (Set (Var "C")) "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 "C")) "holds"   (Bool  "("  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")))) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))) & (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")) ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C"))))  ")" ))) ; 
 
theorem :: FUZZY_1:19 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1: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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:21 (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")) "," (Set (Var "h")) "," (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h1"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h1")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:22 (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"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "g"))))) ; 
 
theorem :: FUZZY_1:23 (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_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:24 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:25 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:26 (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")) "," (Set (Var "h")) "," (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h1"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h1")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:27 (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"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: FUZZY_1:28 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")))))) ; 
 
theorem :: FUZZY_1:29 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")"  ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set (Var "f")))) "holds"  (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:30 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C"))))) "holds"  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")))))) ; 
 
theorem :: FUZZY_1:31 (Bool  "for" (Set (Var "C")) "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 "C"))  "st" (Bool (Bool (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")))))) ; 
 
theorem :: FUZZY_1:32 (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 (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")))) & (Bool (Set (Var "g"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C"))))  ")" )  ")" ))) ; 
 
theorem :: FUZZY_1:33 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool  "("   "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "h1"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h1"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set (Var "h1"))  ($#r1_fuzzy_1 :::"c="::: )  )  ")" )  ")" )  ")" ))) ; 
 
theorem :: FUZZY_1:34 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool  "("   "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set (Var "h"))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set (Var "f"))  ($#r1_fuzzy_1 :::"c="::: )  )  ")" )  ")" )  ")" ))) ; 
 
theorem :: FUZZY_1:35 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C"))  "st" (Bool (Bool (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")" )  ($#r1_fuzzy_1 :::"c="::: )  ) & (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "h")) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C"))))) "holds"  (Bool (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:36 (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 (Set (Var "g"))  ($#r1_fuzzy_1 :::"c="::: )  ) "iff" (Bool (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "f")))  ($#r1_fuzzy_1 :::"c="::: )  )  ")" ))) ; 
 
theorem :: FUZZY_1:37 (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"))  "st" (Bool (Bool (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "g")))  ($#r1_fuzzy_1 :::"c="::: )  )) "holds"  (Bool (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "f")))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:38 (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   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "f")))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:39 (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   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:40 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set  "("  ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")))) & (Bool (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set  "("  ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C"))))  ")" )) ; 
 definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "h", "g" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func "h" :::"\+\"::: "g" ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "C" equals :: FUZZY_1:def 8 (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" "h" "," (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  "g" ")" ) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  "h" ")" ) "," "g" ")"  ")" ) ")" ); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "h")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C"))  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "h")) "," (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "g")) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "h")) ")" ) "," (Set (Var "g")) ")"  ")" ) ")" ))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "h")) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "g")) ")" ) "," (Set (Var "h")) ")"  ")" ) ")" )))
 ; end; 







:: deftheorem    defines :::"\+\"::: FUZZY_1:def 8 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "h"))  ($#k6_fuzzy_1 :::"\+\"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "h")) "," (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "g")) ")" ) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "h")) ")" ) "," (Set (Var "g")) ")"  ")" ) ")" )))); 
 
theorem :: FUZZY_1:41 (Bool  "for" (Set (Var "C")) "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 "C")) "holds"  (Bool (Set (Set (Var "f"))  ($#k6_fuzzy_1 :::"\+\"::: )  (Set  "("  ($#k4_fuzzy_1 :::"EMF"::: )  (Set (Var "C")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: FUZZY_1:42 (Bool  "for" (Set (Var "C")) "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 "C")) "holds"  (Bool (Set (Set (Var "f"))  ($#k6_fuzzy_1 :::"\+\"::: )  (Set  "("  ($#k5_fuzzy_1 :::"UMF"::: )  (Set (Var "C")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "f")))))) ; 
 
theorem :: FUZZY_1:43 (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")) "," (Set (Var "h")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"  (Bool (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set (Var "h")) "," (Set (Var "f")) ")"  ")" ) ")" )  ($#r2_funct_2 :::"="::: )  (Set   ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k2_fuzzy_1 :::"max"::: )   "(" (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "g")) "," (Set (Var "h")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "h")) "," (Set (Var "f")) ")"  ")" ) ")" )))) ; 
 
theorem :: FUZZY_1:44 (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   ($#k3_fuzzy_1 :::"1_minus"::: )  (Set  "(" (Set (Var "f"))  ($#k6_fuzzy_1 :::"\+\"::: )  (Set (Var "g")) ")" ))  ($#r1_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:45 (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_fuzzy_1 :::"c="::: )  ))) ; 
 
theorem :: FUZZY_1:46 (Bool  "for" (Set (Var "C")) "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 "C")) "holds"  (Bool (Set (Set (Var "f"))  ($#k6_fuzzy_1 :::"\+\"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k1_fuzzy_1 :::"min"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k3_fuzzy_1 :::"1_minus"::: )  (Set (Var "f")) ")" ) ")" )))) ; 
 definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "h", "g" be   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Const "C")); func  :::"ab_difMF":::  "(" "h" "," "g" ")"  ->   ($#m1_subset_1 :::"Membership_Func":::) "of" "C" means :: FUZZY_1:def 9 (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "C" "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" "h"  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" "g"  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" )))); end; 







:: deftheorem    defines :::"ab_difMF"::: FUZZY_1:def 9 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "g")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Membership_Func":::) "of" (Set (Var "C")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_fuzzy_1 :::"ab_difMF"::: )   "(" (Set (Var "h")) "," (Set (Var "g")) ")" )) "iff" (Bool  "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "h"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set (Var "c")) ")" ) ")" ))))  ")" )));