let x, y be object ; for X, Y being set
for R being Relation holds
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
let X, Y be set ; for R being Relation holds
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
let R be Relation; ( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
thus
( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies ( not x in Y & not y in X & y in Y ) )
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )proof
assume that A1:
X misses Y
and A2:
(
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R )
and A3:
x in X
;
( not x in Y & not y in X & y in Y )
A4:
not
[x,y] in [:Y,X:]
A6:
(
[x,y] in [:X,Y:] implies ( not
x in Y & not
y in X &
y in Y ) )
[:X,Y:] misses [:Y,X:]
by A1, ZFMISC_1:104;
hence
( not
x in Y & not
y in X &
y in Y )
by A2, A6, A4, XBOOLE_0:5;
verum
end;
thus
( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies ( not y in X & not x in Y & x in X ) )
( ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) ) & ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) ) )
thus
( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies ( not x in X & not y in Y & y in X ) )
( X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies ( not x in X & not y in Y & x in Y ) )proof
assume that A12:
X misses Y
and A13:
(
R c= [:X,Y:] \/ [:Y,X:] &
[x,y] in R )
and A14:
x in Y
;
( not x in X & not y in Y & y in X )
A15:
not
[x,y] in [:X,Y:]
(
[x,y] in [:Y,X:] & not
[x,y] in [:X,Y:] implies ( not
x in X & not
y in Y &
y in X ) )
hence
( not
x in X & not
y in Y &
y in X )
by A13, A15, XBOOLE_0:def 3;
verum
end;
assume that
A17:
X misses Y
and
A18:
( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R )
and
A19:
y in X
; ( not x in X & not y in Y & x in Y )
A20:
not [x,y] in [:X,Y:]
( [x,y] in [:Y,X:] implies ( not x in X & not y in Y & x in Y ) )
hence
( not x in X & not y in Y & x in Y )
by A18, A20, XBOOLE_0:def 3; verum