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

( 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

hence
R = S
by Th1; :: thesis: verum
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;( R . x <= S . x & S . x <= R . x ) by A1;

hence R . x = S . x by XXREAL_0:1; :: thesis: verum