let X be non empty set ; :: thesis: for R, S being Membership_Func of X holds
( R = S iff ( S c= & R c= ) )
let R, S be Membership_Func of X; :: thesis: ( R = S iff ( S c= & R c= ) )
thus ( R = S implies ( S c= & R c= ) ) ; :: thesis: ( S c= & R c= implies R = S )
assume A1: ( S c= & R c= ) ; :: thesis: R = S
for x being Element of X holds R . x = S . x
proof
let x be Element of X; :: thesis: R . x = S . x
( R . x <= S . x & S . x <= R . x ) by A1;
hence R . x = S . x by XXREAL_0:1; :: thesis: verum
end;
hence R = S by Th1; :: thesis: verum