let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C st g c= & h c= & min (g,h) = EMF C holds
f = EMF C
let f, h, g be Membership_Func of C; :: thesis: ( g c= & h c= & min (g,h) = EMF C implies f = EMF C )
assume that
A1: ( g c= & h c= ) and
A2: min (g,h) = EMF C ; :: thesis: f = EMF C
A3: for x being Element of C st x in C holds
f . x = (EMF C) . x

proof

let x be Element of C; :: thesis: ( x in C implies f . x = (EMF C) . x )
( f . x <= g . x & f . x <= h . x ) by A1;
then f . x <= min ((g . x),(h . x)) by XXREAL_0:20;
then A4: f . x <= (min (g,h)) . x by Def3;
(EMF C) . x <= f . x by Th15;
hence ( x in C implies f . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; :: thesis: verum

end;

( C = dom f & C = dom (EMF C) ) by FUNCT_2:def 1;
hence f = EMF C by A3, PARTFUN1:5; :: thesis: verum