let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C st g c= & min (g,h) = EMF C holds

min (f,h) = EMF C

let f, h, g be Membership_Func of C; :: thesis: ( g c= & min (g,h) = EMF C implies min (f,h) = EMF C )

assume that

A1: g c= and

A2: min (g,h) = EMF C ; :: thesis: min (f,h) = EMF C

A3: for x being Element of C st x in C holds

(min (f,h)) . x = (EMF C) . x

hence min (f,h) = EMF C by A3, PARTFUN1:5; :: thesis: verum

min (f,h) = EMF C

let f, h, g be Membership_Func of C; :: thesis: ( g c= & min (g,h) = EMF C implies min (f,h) = EMF C )

assume that

A1: g c= and

A2: min (g,h) = EMF C ; :: thesis: min (f,h) = EMF C

A3: for x being Element of C st x in C holds

(min (f,h)) . x = (EMF C) . x

proof

( C = dom (min (f,h)) & C = dom (EMF C) )
by FUNCT_2:def 1;
let x be Element of C; :: thesis: ( x in C implies (min (f,h)) . x = (EMF C) . 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 . x),(h . x)) <= (min (g,h)) . x by Def3;

then A4: (min (f,h)) . x <= (min (g,h)) . x by Def3;

(EMF C) . x <= (min (f,h)) . x by Th15;

hence ( x in C implies (min (f,h)) . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; :: thesis: verum

end;f . x <= g . x by A1;

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 Def3;

then A4: (min (f,h)) . x <= (min (g,h)) . x by Def3;

(EMF C) . x <= (min (f,h)) . x by Th15;

hence ( x in C implies (min (f,h)) . x = (EMF C) . x ) by A2, A4, XXREAL_0:1; :: thesis: verum

hence min (f,h) = EMF C by A3, PARTFUN1:5; :: thesis: verum