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 Th15;
(min (f,(UMF C))) . x = min ((f . x),((UMF C) . x)) by Def3
.= 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 Th15;
(min (f,(EMF C))) . x = min ((f . x),((EMF C) . x)) by Def3
.= (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 Th15;
(max (f,(EMF C))) . x = max ((f . x),((EMF C) . x)) by Def4
.= 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 Th14, Th16;
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:5; :: thesis: verum