let X, Y, Z, W be set ; :: thesis: for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)
let R be Relation; :: thesis: ( R c= [:X,Y:] & X = Z \/ W implies R = (R | Z) \/ (R | W) )
assume A1: ( R c= [:X,Y:] & X = Z \/ W ) ; :: thesis: R = (R | Z) \/ (R | W)
then A2: ( Z c= X & W c= X ) by XBOOLE_1:7;
thus R = R /\ [:X,Y:] by A1, XBOOLE_1:28
.= R /\ ([:Z,Y:] \/ [:W,Y:]) by A1, ZFMISC_1:120
.= (R /\ [:Z,Y:]) \/ (R /\ [:W,Y:]) by XBOOLE_1:23
.= (R | Z) \/ (R /\ [:W,Y:]) by A1, A2, Th24
.= (R | Z) \/ (R | W) by A1, A2, Th24 ; :: thesis: verum