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 )
A1: ( C = dom (max f,(EMF C)) & C = dom (min f,(EMF C)) ) by FUNCT_2:def 1;
A2: 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;

A4: 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 )
A5: (EMF C) . x <= f . x by Th17;
(min f,(EMF C)) . x = min (f . x),((EMF C) . x) by Def4
.= (EMF C) . x by A5, XXREAL_0:def 9 ;
hence ( x in C implies (min f,(EMF C)) . x = (EMF C) . x ) ; :: thesis: verum

end;

A6: 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 )
A7: (EMF C) . x <= f . x by Th17;
(max f,(EMF C)) . x = max (f . x),((EMF C) . x) by Def5
.= f . x by A7, XXREAL_0:def 10 ;
hence ( x in C implies (max f,(EMF C)) . x = f . x ) ; :: thesis: verum

end;

( 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 )
A8: C = dom (EMF C) by FUNCT_2:def 1;
( C = dom (min f,(UMF C)) & C = dom f ) by FUNCT_2:def 1;
hence ( min f,(UMF C) = f & max f,(EMF C) = f & min f,(EMF C) = EMF C ) by A2, A6, A1, A8, A4, PARTFUN1:34; :: thesis: verum