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