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