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 `) c= Y ` iff (R ~) .: Y c= X )
let X be Subset of A; :: thesis: for Y being Subset of B
for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
let Y be Subset of B; :: thesis: for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
let R be Relation of A,B; :: thesis: ( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
( X ` misses (R ~) .: Y iff Y misses R .: (X `) ) by Th45;
hence ( R .: (X `) c= Y ` iff (R ~) .: Y c= X ) by SUBSET_1:23, SUBSET_1:24; :: thesis: verum