let C be non empty set ; :: thesis: for f, g, h, h1 being Membership_Func of C st g c= & h1 c= holds
min g,h1 c=
let f, g, h, h1 be Membership_Func of C; :: thesis: ( g c= & h1 c= implies min g,h1 c= )
assume A1: ( g c= & h1 c= ) ; :: thesis: min g,h1 c=
let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: (min f,h) . x <= (min g,h1) . x
( f . x <= g . x & h . x <= h1 . x ) by A1, Def3;
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 Def4;
hence (min f,h) . x <= (min g,h1) . x by Def4; :: thesis: verum