let A, B be set ; :: thesis: for X1, X2 being Subset of A
for R being Subset of [:A,B:] st (.: R) .: {_{X1}_} = {} holds
R .:^ (X1 \/ X2) = R .:^ X2
let X1, X2 be Subset of A; :: thesis: for R being Subset of [:A,B:] st (.: R) .: {_{X1}_} = {} holds
R .:^ (X1 \/ X2) = R .:^ X2
let R be Subset of [:A,B:]; :: thesis: ( (.: R) .: {_{X1}_} = {} implies R .:^ (X1 \/ X2) = R .:^ X2 )
A1: {_{(X1 \/ X2)}_} = {_{X1}_} \/ {_{X2}_} by Th3;
assume A2: (.: R) .: {_{X1}_} = {} ; :: thesis: R .:^ (X1 \/ X2) = R .:^ X2
R .:^ (X1 \/ X2) = Intersect (((.: R) .: {_{X1}_}) \/ ((.: R) .: {_{X2}_})) by A1, RELAT_1:120
.= R .:^ X2 by A2 ;
hence R .:^ (X1 \/ X2) = R .:^ X2 ; :: thesis: verum