let C be non empty set ; 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; ( 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
; 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
let x be
Element of
C;
( 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;
verum
end;
( C = dom (min (f,h)) & C = dom (EMF C) )
by FUNCT_2:def 1;
hence
min (f,h) = EMF C
by A3, PARTFUN1:5; verum