let C be non empty set ; 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; ( 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;
( 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 )
;
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;
( 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 )
;
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; verum