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

(min (f,(max (f,g)))) . x = f . x

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

( 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

A3:
for x being Element of C st x in C holds
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;(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

(min (f,(max (f,g)))) . x = f . x

proof

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

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