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

proof

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

end;

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

proof

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

end;

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