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