begin
theorem
for
X,
Y,
x,
y being ( ( ) ( )
set )
for
R being ( (
Relation-like ) (
Relation-like )
Relation) holds
( (
X : ( ( ) ( )
set )
misses Y : ( ( ) ( )
set ) &
R : ( (
Relation-like ) (
Relation-like )
Relation)
c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
\/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) (
Relation-like )
set ) &
[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( )
set )
in R : ( (
Relation-like ) (
Relation-like )
Relation) &
x : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) implies ( not
x : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) & not
y : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) &
y : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) ) ) & (
X : ( ( ) ( )
set )
misses Y : ( ( ) ( )
set ) &
R : ( (
Relation-like ) (
Relation-like )
Relation)
c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
\/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) (
Relation-like )
set ) &
[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( )
set )
in R : ( (
Relation-like ) (
Relation-like )
Relation) &
y : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) implies ( not
y : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) & not
x : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) &
x : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) ) ) & (
X : ( ( ) ( )
set )
misses Y : ( ( ) ( )
set ) &
R : ( (
Relation-like ) (
Relation-like )
Relation)
c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
\/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) (
Relation-like )
set ) &
[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( )
set )
in R : ( (
Relation-like ) (
Relation-like )
Relation) &
x : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) implies ( not
x : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) & not
y : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) &
y : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) ) ) & (
X : ( ( ) ( )
set )
misses Y : ( ( ) ( )
set ) &
R : ( (
Relation-like ) (
Relation-like )
Relation)
c= [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set )
\/ [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
Relation-like )
set ) : ( ( ) (
Relation-like )
set ) &
[x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( )
set )
in R : ( (
Relation-like ) (
Relation-like )
Relation) &
y : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) implies ( not
x : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) & not
y : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) &
x : ( ( ) ( )
set )
in Y : ( ( ) ( )
set ) ) ) ) ;