let A, B be set ; :: thesis: for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
let X be Subset of A; :: thesis: for Y being Subset of B
for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
let Y be Subset of B; :: thesis: for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
let R be Relation of A,B; :: thesis: ( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
A1: R .:^ X c= R .:^ ((R ~) .:^ (R .:^ X)) by Th60;
X c= (R ~) .:^ (R .:^ X) by Th60;
then R .:^ ((R ~) .:^ (R .:^ X)) c= R .:^ X by Th31;
hence R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) by A1; :: thesis: (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y))
thus (R ~) .:^ Y c= (R ~) .:^ (R .:^ ((R ~) .:^ Y)) by Th60; :: according to XBOOLE_0:def 10 :: thesis: (R ~) .:^ (R .:^ ((R ~) .:^ Y)) c= (R ~) .:^ Y
Y c= R .:^ ((R ~) .:^ Y) by Th60;
hence (R ~) .:^ (R .:^ ((R ~) .:^ Y)) c= (R ~) .:^ Y by Th31; :: thesis: verum