let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2 st min (f,g) = Zmf (C1,C2) holds
f \ g = f
let f, g be RMembership_Func of C1,C2; :: thesis: ( min (f,g) = Zmf (C1,C2) implies f \ g = f )
Zmf (C1,C2) = EMF [:C1,C2:] ;
hence ( min (f,g) = Zmf (C1,C2) implies f \ g = f ) by Th27; :: thesis: verum