let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds
( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f )
let f, g be Membership_Func of C; :: thesis: ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f )
A1: C = dom (min (f,(max (f,g)))) by FUNCT_2:def 1;
A2: for x being Element of C st x in C holds
(max (f,(min (f,g)))) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (max (f,(min (f,g)))) . x = f . x )
(max (f,(min (f,g)))) . x = max ((f . x),((min (f,g)) . x)) by Def4
.= max ((f . x),(min ((f . x),(g . x)))) by Def3
.= f . x by XXREAL_0:36 ;
hence ( x in C implies (max (f,(min (f,g)))) . x = f . x ) ; :: thesis: verum

end;

A3: for x being Element of C st x in C holds
(min (f,(max (f,g)))) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (min (f,(max (f,g)))) . x = f . x )
(min (f,(max (f,g)))) . x = min ((f . x),((max (f,g)) . x)) by Def3
.= min ((f . x),(max ((f . x),(g . x)))) by Def4
.= f . x by XXREAL_0:35 ;
hence ( x in C implies (min (f,(max (f,g)))) . x = f . x ) ; :: thesis: verum

end;

( C = dom (max (f,(min (f,g)))) & C = dom f ) by FUNCT_2:def 1;
hence ( max (f,(min (f,g))) = f & min (f,(max (f,g))) = f ) by A1, A2, A3, PARTFUN1:5; :: thesis: verum