let C be non empty set ; :: thesis: for h, f, g being Membership_Func of C st f c= & g c= holds
min (f,g) c=
let h, f, g be Membership_Func of C; :: thesis: ( f c= & g c= implies min (f,g) c= )
assume A1: ( f c= & g c= ) ; :: thesis: min (f,g) c=
let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: h . x <= (min (f,g)) . x
( h . x <= f . x & h . x <= g . x ) by A1, Def3;
then h . x <= min ((f . x),(g . x)) by XXREAL_0:20;
hence h . x <= (min (f,g)) . x by Def4; :: thesis: verum