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

proof

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

end;

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

proof

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

end;

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