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