let A, B be set ; :: thesis: for X being Subset of
for Y being Subset of
for R being Relation of , holds
( R .: (X ` ) c= Y ` iff (R ~ ) .: Y c= X )
let X be Subset of ; :: thesis: for Y being Subset of
for R being Relation of , holds
( R .: (X ` ) c= Y ` iff (R ~ ) .: Y c= X )
let Y be Subset of ; :: thesis: for R being Relation of , holds
( R .: (X ` ) c= Y ` iff (R ~ ) .: Y c= X )
let R be Relation of ,; :: thesis: ( R .: (X ` ) c= Y ` iff (R ~ ) .: Y c= X )
( X ` misses (R ~ ) .: Y iff Y misses R .: (X ` ) ) by Th46;
hence ( R .: (X ` ) c= Y ` iff (R ~ ) .: Y c= X ) by SUBSET_1:43, SUBSET_1:44; :: thesis: verum