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 that
A1: R c= [:X,Y:] and
A2: X = Z \/ W ; :: thesis: R = (R | Z) \/ (R | W)
thus R = R /\ [:X,Y:] by A1, XBOOLE_1:28
.= R /\ ([:Z,Y:] \/ [:W,Y:]) by A2, ZFMISC_1:97
.= (R /\ [:Z,Y:]) \/ (R /\ [:W,Y:]) by XBOOLE_1:23
.= (R | Z) \/ (R /\ [:W,Y:]) by A1, Th8
.= (R | Z) \/ (R | W) by A1, Th8 ; :: thesis: verum