let X, Y be set ; :: thesis: for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds
R | X c= [:X,Y:]
let R be Relation; :: thesis: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] implies R | X c= [:X,Y:] )
assume that
A1: X /\ Y = {} and
A2: R c= [:X,Y:] \/ [:Y,X:] ; :: according to XBOOLE_0:def 7 :: thesis: R | X c= [:X,Y:]
R | X = R /\ [:X,(rng R):] by RELAT_1:67;
then R | X c= ([:X,Y:] \/ [:Y,X:]) /\ [:X,(rng R):] by A2, XBOOLE_1:26;
then A3: R | X c= ([:X,Y:] /\ [:X,(rng R):]) \/ ([:Y,X:] /\ [:X,(rng R):]) by XBOOLE_1:23;
[:Y,X:] /\ [:X,(rng R):] = [:(X /\ Y),(X /\ (rng R)):] by ZFMISC_1:100
.= {} by A1, ZFMISC_1:90 ;
hence R | X c= [:X,Y:] by A3, XBOOLE_1:18; :: thesis: verum