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 Th61;
X c= (R ~ ) .:^ (R .:^ X) by Th61;
then R .:^ ((R ~ ) .:^ (R .:^ X)) c= R .:^ X by Th32;
hence R .:^ X = R .:^ ((R ~ ) .:^ (R .:^ X)) by A1, XBOOLE_0:def 10; :: thesis: (R ~ ) .:^ Y = (R ~ ) .:^ (R .:^ ((R ~ ) .:^ Y))
thus (R ~ ) .:^ Y c= (R ~ ) .:^ (R .:^ ((R ~ ) .:^ Y)) by Th61; :: according to XBOOLE_0:def 10 :: thesis: (R ~ ) .:^ (R .:^ ((R ~ ) .:^ Y)) c= (R ~ ) .:^ Y
Y c= R .:^ ((R ~ ) .:^ Y) by Th61;
hence (R ~ ) .:^ (R .:^ ((R ~ ) .:^ Y)) c= (R ~ ) .:^ Y by Th32; :: thesis: verum