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

proof

let x be Element of C; :: thesis: ( x in C implies (min f,h) . x = (EMF C) . x )
( f . x <= g . x & min g,h = EMF C ) by A1, Def3;
then min (f . x),(h . x) <= min (g . x),(h . x) by XXREAL_0:18;
then min (f . x),(h . x) <= (min g,h) . x by Def4;
then A3: (min f,h) . x <= (min g,h) . x by Def4;
(EMF C) . x <= (min f,h) . x by Th17;
hence ( x in C implies (min f,h) . x = (EMF C) . x ) by A1, A3, XXREAL_0:1; :: thesis: verum

end;

hence min f,h = EMF C by A2, PARTFUN1:34; :: thesis: verum