let A, B be set ; for R being Subset of [:A,B:]
for X, Y being set holds
( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
let R be Subset of [:A,B:]; for X, Y being set holds
( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
let X, Y be set ; ( X meets (R ~) .: Y iff ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) )
hereby ( ex x, y being set st
( x in X & y in Y & x in Im ((R ~),y) ) implies X meets (R ~) .: Y )
assume
X meets (R ~) .: Y
;
ex a, b being set st
( a in X & b in Y & a in Im ((R ~),b) )then consider a being
object such that A1:
a in X
and A2:
a in (R ~) .: Y
by XBOOLE_0:3;
consider b being
object such that A3:
[b,a] in R ~
and A4:
b in Y
by A2, RELAT_1:def 13;
A5:
b in {b}
by TARSKI:def 1;
reconsider a =
a,
b =
b as
set by TARSKI:1;
take a =
a;
ex b being set st
( a in X & b in Y & a in Im ((R ~),b) )take b =
b;
( a in X & b in Y & a in Im ((R ~),b) )thus
a in X
by A1;
( b in Y & a in Im ((R ~),b) )thus
b in Y
by A4;
a in Im ((R ~),b)thus
a in Im (
(R ~),
b)
by A3, A5, RELAT_1:def 13;
verum
end;
given x, y being set such that A6:
x in X
and
A7:
y in Y
and
A8:
x in Im ((R ~),y)
; X meets (R ~) .: Y
ex a being object st
( [a,x] in R ~ & a in {y} )
by A8, RELAT_1:def 13;
then
[y,x] in R ~
by TARSKI:def 1;
then
x in (R ~) .: Y
by A7, RELAT_1:def 13;
hence
X meets (R ~) .: Y
by A6, XBOOLE_0:3; verum