let X, Z be set ; :: thesis: for Y being Relation st Z c= Y & not X \ Z is with_pair holds
X \ Y = X \ Z
let Y be Relation; :: thesis: ( Z c= Y & not X \ Z is with_pair implies X \ Y = X \ Z )
assume A1: Z c= Y ; :: thesis: ( X \ Z is with_pair or X \ Y = X \ Z )
assume A2: not X \ Z is with_pair ; :: thesis: X \ Y = X \ Z

now

given x being set such that A3: x in (Y \ Z) /\ (X \ Z) ; :: thesis: contradiction
A4: ( x in Y \ Z & x in X \ Z ) by A3, XBOOLE_0:def 4;
then ex a, b being set st x = [a,b] by RELAT_1:def 1;
hence contradiction by A2, A4, FACIRC_1:def 2; :: thesis: verum

end;

then (Y \ Z) /\ (X \ Z) = {} by XBOOLE_0:7;
then Y \ Z misses X \ Z by XBOOLE_0:def 7;
then A5: (X \ Z) \ (Y \ Z) = X \ Z by XBOOLE_1:83;
X \ Y = X \ ((Y \ Z) \/ Z) by A1, XBOOLE_1:45
.= X \ Z by A5, XBOOLE_1:41 ;
hence X \ Y = X \ Z ; :: thesis: verum