let X be Relation; :: thesis: for Y, Z being set st Z c= Y & not Y \ Z is with_pair holds
X \ Y = X \ Z
let Y, Z be set ; :: thesis: ( Z c= Y & not Y \ Z is with_pair implies X \ Y = X \ Z )
assume A1: Z c= Y ; :: thesis: ( Y \ Z is with_pair or X \ Y = X \ Z )
assume not Y \ Z is with_pair ; :: thesis: X \ Y = X \ Z
then for x being set holds not x in X /\ (Y \ Z) ;
then X /\ (Y \ Z) = {} by XBOOLE_0:7;
then X misses Y \ Z by XBOOLE_0:def 7;
then A2: X \ (Y \ Z) = X 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