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
( X c= (R ~ ) .:^ Y iff Y c= R .:^ X )
let X be Subset of A; :: thesis: for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~ ) .:^ Y iff Y c= R .:^ X )
let Y be Subset of B; :: thesis: for R being Relation of A,B holds
( X c= (R ~ ) .:^ Y iff Y c= R .:^ X )
let R be Relation of A,B; :: thesis: ( X c= (R ~ ) .:^ Y iff Y c= R .:^ X )
( X c= (R ~ ) .:^ Y iff X misses ((R ~ ) .:^ Y) ` ) by SUBSET_1:44;
then ( X c= (R ~ ) .:^ Y iff X misses ((R ~ ) ` ) .: Y ) by Th49;
then A1: ( X c= (R ~ ) .:^ Y iff X /\ (((R ~ ) ` ) .: Y) = {} ) by XBOOLE_0:def 7;
reconsider S = R ` as Relation of A,B ;
( X misses (S ~ ) .: Y iff Y misses S .: X ) by Th46;
then ( X /\ ((S ~ ) .: Y) = {} iff Y /\ (S .: X) = {} ) by XBOOLE_0:def 7;
then ( X c= (R ~ ) .:^ Y iff ((R .:^ X) ` ) /\ Y = {} ) by A1, Th49, Th60;
then ( X c= (R ~ ) .:^ Y iff (R .:^ X) ` misses Y ) by XBOOLE_0:def 7;
hence ( X c= (R ~ ) .:^ Y iff Y c= R .:^ X ) by SUBSET_1:44; :: thesis: verum