let C be non empty set ; :: thesis: for x being Element of C
for h being Membership_Func of C holds
( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
let x be Element of C; :: thesis: for h being Membership_Func of C holds
( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
let h be Membership_Func of C; :: thesis: ( (EMF C) . x <= h . x & h . x <= (UMF C) . x )
( h c= & UMF C c= ) by Th15, Th16;
hence ( (EMF C) . x <= h . x & h . x <= (UMF C) . x ) by Def3; :: thesis: verum