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 Th32; :: thesis: verum