let X, Z be set ; :: thesis: for Y being Relation st Z c= Y & X \ Z is without_pairs holds

X \ Y = X \ Z

let Y be Relation; :: thesis: ( Z c= Y & X \ Z is without_pairs implies X \ Y = X \ Z )

assume A1: Z c= Y ; :: thesis: ( not X \ Z is without_pairs or X \ Y = X \ Z )

assume X \ Z is without_pairs ; :: thesis: X \ Y = X \ Z

then for x being object holds not x in (Y \ Z) /\ (X \ Z) ;

then (Y \ Z) /\ (X \ Z) = {} by XBOOLE_0:7;

then Y \ Z misses X \ Z by XBOOLE_0:def 7;

then A2: (X \ Z) \ (Y \ Z) = X \ Z by XBOOLE_1:83;

X \ Y = X \ ((Y \ Z) \/ Z) by A1, XBOOLE_1:45

.= X \ Z by A2, XBOOLE_1:41 ;

hence X \ Y = X \ Z ; :: thesis: verum

X \ Y = X \ Z

let Y be Relation; :: thesis: ( Z c= Y & X \ Z is without_pairs implies X \ Y = X \ Z )

assume A1: Z c= Y ; :: thesis: ( not X \ Z is without_pairs or X \ Y = X \ Z )

assume X \ Z is without_pairs ; :: thesis: X \ Y = X \ Z

then for x being object holds not x in (Y \ Z) /\ (X \ Z) ;

then (Y \ Z) /\ (X \ Z) = {} by XBOOLE_0:7;

then Y \ Z misses X \ Z by XBOOLE_0:def 7;

then A2: (X \ Z) \ (Y \ Z) = X \ Z by XBOOLE_1:83;

X \ Y = X \ ((Y \ Z) \/ Z) by A1, XBOOLE_1:45

.= X \ Z by A2, XBOOLE_1:41 ;

hence X \ Y = X \ Z ; :: thesis: verum