let C be non empty set ; for f, h, g being Membership_Func of C holds
( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) ) )
let f, h, g be Membership_Func of C; ( f = max (g,h) iff ( f c= & f c= & ( for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c= ) ) )
assume that
A3:
( f c= & f c= )
and
A4:
for h1 being Membership_Func of C st h1 c= & h1 c= holds
h1 c=
; f = max (g,h)
( max (g,h) c= & max (g,h) c= )
by Th16;
then A5:
max (g,h) c=
by A4;
f c=
by A3, Th18;
hence
f = max (g,h)
by A5, Lm1; verum