let C be non empty set ; :: thesis: for f being Membership_Func of C holds
( max f,(UMF C) = UMF C & min f,(UMF C) = f & max f,(EMF C) = f & min f,(EMF C) = EMF C )
let f be Membership_Func of C; :: thesis: ( max f,(UMF C) = UMF C & min f,(UMF C) = f & max f,(EMF C) = f & min f,(EMF C) = EMF C )
( UMF C c= & max f,(UMF C) c= ) by Th16, Th18;
hence max f,(UMF C) = UMF C by Lm1; :: thesis: ( min f,(UMF C) = f & max f,(EMF C) = f & min f,(EMF C) = EMF C )
A1: min f,(UMF C) = f

proof

A2: ( C = dom (min f,(UMF C)) & C = dom f ) by FUNCT_2:def 1;
for x being Element of C st x in C holds
(min f,(UMF C)) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (min f,(UMF C)) . x = f . x )
A3: f . x <= (UMF C) . x by Th17;
(min f,(UMF C)) . x = min (f . x),((UMF C) . x) by Def4
.= f . x by A3, XXREAL_0:def 9 ;
hence ( x in C implies (min f,(UMF C)) . x = f . x ) ; :: thesis: verum

end;

hence min f,(UMF C) = f by A2, PARTFUN1:34; :: thesis: verum

end;

A4: max f,(EMF C) = f

proof

A5: ( C = dom (max f,(EMF C)) & C = dom f ) by FUNCT_2:def 1;
for x being Element of C st x in C holds
(max f,(EMF C)) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (max f,(EMF C)) . x = f . x )
A6: (EMF C) . x <= f . x by Th17;
(max f,(EMF C)) . x = max (f . x),((EMF C) . x) by Def5
.= f . x by A6, XXREAL_0:def 10 ;
hence ( x in C implies (max f,(EMF C)) . x = f . x ) ; :: thesis: verum

end;

hence max f,(EMF C) = f by A5, PARTFUN1:34; :: thesis: verum

end;

min f,(EMF C) = EMF C

proof

A7: ( C = dom (min f,(EMF C)) & C = dom (EMF C) ) by FUNCT_2:def 1;
for x being Element of C st x in C holds
(min f,(EMF C)) . x = (EMF C) . x

proof

let x be Element of C; :: thesis: ( x in C implies (min f,(EMF C)) . x = (EMF C) . x )
A8: (EMF C) . x <= f . x by Th17;
(min f,(EMF C)) . x = min (f . x),((EMF C) . x) by Def4
.= (EMF C) . x by A8, XXREAL_0:def 9 ;
hence ( x in C implies (min f,(EMF C)) . x = (EMF C) . x ) ; :: thesis: verum

end;

hence min f,(EMF C) = EMF C by A7, PARTFUN1:34; :: thesis: verum

end;

hence ( min f,(UMF C) = f & max f,(EMF C) = f & min f,(EMF C) = EMF C ) by A1, A4; :: thesis: verum