let X, Y, Z, W be set ; for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)
let R be Relation; ( 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
; 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
; verum