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:24;
then ( X c= (R ~) .:^ Y iff X misses ((R ~) `) .: Y ) by Th48;
then A1: ( X c= (R ~) .:^ Y iff X /\ (((R ~) `) .: Y) = {} ) ;
reconsider S = R ` as Relation of A,B ;
( X misses (S ~) .: Y iff Y misses S .: X ) by Th45;
then ( X /\ ((S ~) .: Y) = {} iff Y /\ (S .: X) = {} ) ;
then ( X c= (R ~) .:^ Y iff ((R .:^ X) `) /\ Y = {} ) by A1, Th48, Th59;
then ( X c= (R ~) .:^ Y iff (R .:^ X) ` misses Y ) ;
hence ( X c= (R ~) .:^ Y iff Y c= R .:^ X ) by SUBSET_1:24; :: thesis: verum