let A, B be set ; :: thesis: for X being Subset of A
for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
let X be Subset of A; :: thesis: for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
let Y be Subset of B; :: thesis: for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
let R be Subset of [:A,B:]; :: thesis: ( X misses (R ~) .: Y iff Y misses R .: X )
( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) ) by Th43;
hence ( X misses (R ~) .: Y iff Y misses R .: X ) by Th44; :: thesis: verum