Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isibg2aa Unicode version

Theorem isibg2aa 26112
Description: Properties of an incidence-betweenness geometry. (Contributed by FL, 10-Aug-2016.)
Hypotheses
Ref Expression
isibg2aa.1  |-  P  =  (PPoints `  G )
isibg2aa.2  |-  L  =  (PLines `  G )
isibg2aa.3  |-  B  =  (btw `  G )
isibg2aa.4  |-  C  =  (coln `  G )
isibg2aa.5  |-  ( ph  ->  X  e.  P )
isibg2aa.6  |-  ( ph  ->  Y  e.  P )
isibg2aa.7  |-  ( ph  ->  Z  e.  P )
isibg2aa.8  |-  ( ph  ->  M  e.  L )
isibg2aa.9  |-  ( ph  ->  G  e. Ibg )
Assertion
Ref Expression
isibg2aa  |-  ( ph  ->  ( ( X  =/= 
Y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  ( a B Y )  /\  b  e.  ( X B Y )  /\  Y  e.  ( X B c ) ) )  /\  ( ( ( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) )  ->  (
( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) ) )  /\  ( ( X  e/  M  /\  Y  e/  M  /\  Z  e/  M )  ->  ( ( ( ( ( X B Y )  i^i  M
)  =  (/)  /\  (
( Y B Z )  i^i  M )  =  (/) )  ->  (
( X B Z )  i^i  M )  =  (/) )  /\  (
( ( ( X B Y )  i^i 
M )  =/=  (/)  /\  (
( Y B Z )  i^i  M )  =/=  (/) )  ->  (
( X B Z )  i^i  M )  =  (/) ) ) ) ) ) ) )
Distinct variable groups:    a, b,
c, B    P, a,
b, c    X, a,
b, c    Y, a,
b, c
Allowed substitution hints:    ph( a, b, c)    C( a, b, c)    G( a, b, c)    L( a, b, c)    M( a, b, c)    Z( a, b, c)

Proof of Theorem isibg2aa
Dummy variables  l  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isibg2aa.9 . 2  |-  ( ph  ->  G  e. Ibg )
2 isibg2aa.1 . . . 4  |-  P  =  (PPoints `  G )
3 isibg2aa.2 . . . 4  |-  L  =  (PLines `  G )
4 isibg2aa.3 . . . 4  |-  B  =  (btw `  G )
5 isibg2aa.4 . . . 4  |-  C  =  (coln `  G )
62, 3, 4, 5isibg2 26110 . . 3  |-  ( G  e. Ibg 
<->  ( G  e. Ig  /\  A. x  e.  P  A. y  e.  P  (
( x  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( x  e.  (
a B y )  /\  b  e.  ( x B y )  /\  y  e.  ( x B c ) ) )  /\  A. z  e.  P  (
( ( { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) )  ->  (
( x  e.  ( y B z )  /\  y  e/  (
x B z )  /\  z  e/  (
x B y ) )  \/  ( x  e/  ( y B z )  /\  y  e.  ( x B z )  /\  z  e/  ( x B y ) )  \/  (
x  e/  ( y B z )  /\  y  e/  ( x B z )  /\  z  e.  ( x B y ) ) ) )  /\  ( ( y  e.  ( x B z )  ->  (
y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) ) ) ) ) ) )
7 isibg2aa.5 . . . . . . 7  |-  ( ph  ->  X  e.  P )
8 isibg2aa.6 . . . . . . 7  |-  ( ph  ->  Y  e.  P )
9 neeq1 2454 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  =/=  y  <->  X  =/=  y ) )
10 eleq1 2343 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
x  e.  ( a B y )  <->  X  e.  ( a B y ) ) )
11 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x B y )  =  ( X B y ) )
1211eleq2d 2350 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
b  e.  ( x B y )  <->  b  e.  ( X B y ) ) )
13 oveq1 5865 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x B c )  =  ( X B c ) )
1413eleq2d 2350 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
y  e.  ( x B c )  <->  y  e.  ( X B c ) ) )
1510, 12, 143anbi123d 1252 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  (
( x  e.  ( a B y )  /\  b  e.  ( x B y )  /\  y  e.  ( x B c ) )  <->  ( X  e.  ( a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) ) ) )
1615rexbidv 2564 . . . . . . . . . . . 12  |-  ( x  =  X  ->  ( E. c  e.  P  ( x  e.  (
a B y )  /\  b  e.  ( x B y )  /\  y  e.  ( x B c ) )  <->  E. c  e.  P  ( X  e.  (
a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) ) ) )
17162rexbidv 2586 . . . . . . . . . . 11  |-  ( x  =  X  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  ( x  e.  (
a B y )  /\  b  e.  ( x B y )  /\  y  e.  ( x B c ) )  <->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  (
a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) ) ) )
189, 17imbi12d 311 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( x  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( x  e.  (
a B y )  /\  b  e.  ( x B y )  /\  y  e.  ( x B c ) ) )  <->  ( X  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  ( a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) ) ) ) )
19 tpeq1 3715 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  { x ,  y ,  z }  =  { X ,  y ,  z } )
2019eleq1d 2349 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  ( { x ,  y ,  z }  e.  C 
<->  { X ,  y ,  z }  e.  C ) )
21 neeq1 2454 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  =/=  z  <->  X  =/=  z ) )
229, 213anbi12d 1253 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
)  <->  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z ) ) )
2320, 22anbi12d 691 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  (
( { x ,  y ,  z }  e.  C  /\  (
x  =/=  y  /\  x  =/=  z  /\  y  =/=  z ) )  <->  ( { X ,  y , 
z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) ) )
24 eleq1 2343 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  e.  ( y B z )  <->  X  e.  ( y B z ) ) )
25 eqidd 2284 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  y  =  y )
26 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
x B z )  =  ( X B z ) )
2725, 26neleq12d 24933 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
y  e/  ( x B z )  <->  y  e/  ( X B z ) ) )
28 eqidd 2284 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  z  =  z )
2928, 11neleq12d 24933 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
z  e/  ( x B y )  <->  z  e/  ( X B y ) ) )
3024, 27, 293anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( x  e.  ( y B z )  /\  y  e/  (
x B z )  /\  z  e/  (
x B y ) )  <->  ( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) ) ) )
31 neleq1 2537 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  e/  ( y B z )  <->  X  e/  ( y B z ) ) )
3226eleq2d 2350 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
y  e.  ( x B z )  <->  y  e.  ( X B z ) ) )
3331, 32, 293anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( x  e/  (
y B z )  /\  y  e.  ( x B z )  /\  z  e/  (
x B y ) )  <->  ( X  e/  ( y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) ) ) )
3411eleq2d 2350 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
z  e.  ( x B y )  <->  z  e.  ( X B y ) ) )
3531, 27, 343anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( x  e/  (
y B z )  /\  y  e/  (
x B z )  /\  z  e.  ( x B y ) )  <->  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )
3630, 33, 353orbi123d 1251 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  (
( ( x  e.  ( y B z )  /\  y  e/  ( x B z )  /\  z  e/  ( x B y ) )  \/  (
x  e/  ( y B z )  /\  y  e.  ( x B z )  /\  z  e/  ( x B y ) )  \/  ( x  e/  (
y B z )  /\  y  e/  (
x B z )  /\  z  e.  ( x B y ) ) )  <->  ( ( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) ) )
3723, 36imbi12d 311 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
( ( { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) )  ->  (
( x  e.  ( y B z )  /\  y  e/  (
x B z )  /\  z  e/  (
x B y ) )  \/  ( x  e/  ( y B z )  /\  y  e.  ( x B z )  /\  z  e/  ( x B y ) )  \/  (
x  e/  ( y B z )  /\  y  e/  ( x B z )  /\  z  e.  ( x B y ) ) ) )  <-> 
( ( { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) )  ->  (
( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  (
y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) ) ) )
38 oveq2 5866 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
z B x )  =  ( z B X ) )
3938eleq2d 2350 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
y  e.  ( z B x )  <->  y  e.  ( z B X ) ) )
4039, 20, 223anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  (
x  =/=  y  /\  x  =/=  z  /\  y  =/=  z ) )  <->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) ) )
4132, 40imbi12d 311 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  (
( y  e.  ( x B z )  ->  ( y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) ) )  <->  ( y  e.  ( X B z )  ->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) ) ) )
42 neleq1 2537 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
x  e/  l  <->  X  e/  l ) )
43423anbi1d 1256 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  <->  ( X  e/  l  /\  y  e/  l  /\  z  e/  l
) ) )
4411ineq1d 3369 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  X  ->  (
( x B y )  i^i  l )  =  ( ( X B y )  i^i  l ) )
4544eqeq1d 2291 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
( ( x B y )  i^i  l
)  =  (/)  <->  ( ( X B y )  i^i  l )  =  (/) ) )
4645anbi1d 685 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  <->  ( (
( X B y )  i^i  l )  =  (/)  /\  (
( y B z )  i^i  l )  =  (/) ) ) )
4726ineq1d 3369 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
( x B z )  i^i  l )  =  ( ( X B z )  i^i  l ) )
4847eqeq1d 2291 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  (
( ( x B z )  i^i  l
)  =  (/)  <->  ( ( X B z )  i^i  l )  =  (/) ) )
4946, 48imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
( ( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l )  =  (/) )  ->  ( ( x B z )  i^i  l )  =  (/) ) 
<->  ( ( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) )
5044neeq1d 2459 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  X  ->  (
( ( x B y )  i^i  l
)  =/=  (/)  <->  ( ( X B y )  i^i  l )  =/=  (/) ) )
5150anbi1d 685 . . . . . . . . . . . . . . . . 17  |-  ( x  =  X  ->  (
( ( ( x B y )  i^i  l )  =/=  (/)  /\  (
( y B z )  i^i  l )  =/=  (/) )  <->  ( (
( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) ) ) )
5251, 48imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  (
( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  <->  ( (
( ( X B y )  i^i  l
)  =/=  (/)  /\  (
( y B z )  i^i  l )  =/=  (/) )  ->  (
( X B z )  i^i  l )  =  (/) ) ) )
5349, 52anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
( ( ( ( ( x B y )  i^i  l )  =  (/)  /\  (
( y B z )  i^i  l )  =  (/) )  ->  (
( x B z )  i^i  l )  =  (/) )  /\  (
( ( ( x B y )  i^i  l )  =/=  (/)  /\  (
( y B z )  i^i  l )  =/=  (/) )  ->  (
( x B z )  i^i  l )  =  (/) ) )  <->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) )
5443, 53imbi12d 311 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) )  <->  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) )
5554ralbidv 2563 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  ( A. l  e.  L  ( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) )  <->  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) )
5641, 55anbi12d 691 . . . . . . . . . . . 12  |-  ( x  =  X  ->  (
( ( y  e.  ( x B z )  ->  ( y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) ) )  <->  ( (
y  e.  ( X B z )  -> 
( y  e.  ( z B X )  /\  { X , 
y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) ) )
5737, 56anbi12d 691 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
( ( ( { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) )  ->  (
( x  e.  ( y B z )  /\  y  e/  (
x B z )  /\  z  e/  (
x B y ) )  \/  ( x  e/  ( y B z )  /\  y  e.  ( x B z )  /\  z  e/  ( x B y ) )  \/  (
x  e/  ( y B z )  /\  y  e/  ( x B z )  /\  z  e.  ( x B y ) ) ) )  /\  ( ( y  e.  ( x B z )  ->  (
y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) ) ) )  <->  ( (
( { X , 
y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z ) )  -> 
( ( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )  /\  ( ( y  e.  ( X B z )  ->  (
y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) ) ) )
5857ralbidv 2563 . . . . . . . . . 10  |-  ( x  =  X  ->  ( A. z  e.  P  ( ( ( { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) )  ->  (
( x  e.  ( y B z )  /\  y  e/  (
x B z )  /\  z  e/  (
x B y ) )  \/  ( x  e/  ( y B z )  /\  y  e.  ( x B z )  /\  z  e/  ( x B y ) )  \/  (
x  e/  ( y B z )  /\  y  e/  ( x B z )  /\  z  e.  ( x B y ) ) ) )  /\  ( ( y  e.  ( x B z )  ->  (
y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) ) ) )  <->  A. z  e.  P  ( (
( { X , 
y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z ) )  -> 
( ( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )  /\  ( ( y  e.  ( X B z )  ->  (
y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) ) ) )
5918, 58anbi12d 691 . . . . . . . . 9  |-  ( x  =  X  ->  (
( ( x  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( x  e.  ( a B y )  /\  b  e.  ( x B y )  /\  y  e.  ( x B c ) ) )  /\  A. z  e.  P  ( ( ( { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) )  ->  (
( x  e.  ( y B z )  /\  y  e/  (
x B z )  /\  z  e/  (
x B y ) )  \/  ( x  e/  ( y B z )  /\  y  e.  ( x B z )  /\  z  e/  ( x B y ) )  \/  (
x  e/  ( y B z )  /\  y  e/  ( x B z )  /\  z  e.  ( x B y ) ) ) )  /\  ( ( y  e.  ( x B z )  ->  (
y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) ) ) ) )  <-> 
( ( X  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  ( a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) ) )  /\  A. z  e.  P  ( ( ( { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) )  ->  (
( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  (
y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )  /\  ( ( y  e.  ( X B z )  ->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) ) ) ) )
60 neeq2 2455 . . . . . . . . . . 11  |-  ( y  =  Y  ->  ( X  =/=  y  <->  X  =/=  Y ) )
61 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
a B y )  =  ( a B Y ) )
6261eleq2d 2350 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  ( X  e.  ( a B y )  <->  X  e.  ( a B Y ) ) )
63 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  ( X B y )  =  ( X B Y ) )
6463eleq2d 2350 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
b  e.  ( X B y )  <->  b  e.  ( X B Y ) ) )
65 eleq1 2343 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
y  e.  ( X B c )  <->  Y  e.  ( X B c ) ) )
6662, 64, 653anbi123d 1252 . . . . . . . . . . . . 13  |-  ( y  =  Y  ->  (
( X  e.  ( a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) )  <->  ( X  e.  ( a B Y )  /\  b  e.  ( X B Y )  /\  Y  e.  ( X B c ) ) ) )
6766rexbidv 2564 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  ( E. c  e.  P  ( X  e.  (
a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) )  <->  E. c  e.  P  ( X  e.  (
a B Y )  /\  b  e.  ( X B Y )  /\  Y  e.  ( X B c ) ) ) )
68672rexbidv 2586 . . . . . . . . . . 11  |-  ( y  =  Y  ->  ( E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  (
a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) )  <->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  (
a B Y )  /\  b  e.  ( X B Y )  /\  Y  e.  ( X B c ) ) ) )
6960, 68imbi12d 311 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
( X  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  (
a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) ) )  <->  ( X  =/=  Y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  ( a B Y )  /\  b  e.  ( X B Y )  /\  Y  e.  ( X B c ) ) ) ) )
70 tpeq2 3716 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  { X ,  y ,  z }  =  { X ,  Y ,  z } )
7170eleq1d 2349 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  ( { X ,  y ,  z }  e.  C  <->  { X ,  Y , 
z }  e.  C
) )
72 neeq1 2454 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
y  =/=  z  <->  Y  =/=  z ) )
7360, 723anbi13d 1254 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
)  <->  ( X  =/= 
Y  /\  X  =/=  z  /\  Y  =/=  z
) ) )
7471, 73anbi12d 691 . . . . . . . . . . . . 13  |-  ( y  =  Y  ->  (
( { X , 
y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z ) )  <->  ( { X ,  Y , 
z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z
) ) ) )
75 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
y B z )  =  ( Y B z ) )
7675eleq2d 2350 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  ( X  e.  ( y B z )  <->  X  e.  ( Y B z ) ) )
77 neleq1 2537 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
y  e/  ( X B z )  <->  Y  e/  ( X B z ) ) )
78 eqidd 2284 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  z  =  z )
7978, 63neleq12d 24933 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
z  e/  ( X B y )  <->  z  e/  ( X B Y ) ) )
8076, 77, 793anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  <->  ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) ) ) )
81 eqidd 2284 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  X  =  X )
8281, 75neleq12d 24933 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  ( X  e/  ( y B z )  <->  X  e/  ( Y B z ) ) )
83 eleq1 2343 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
y  e.  ( X B z )  <->  Y  e.  ( X B z ) ) )
8482, 83, 793anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
( X  e/  (
y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  <-> 
( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) ) ) )
8563eleq2d 2350 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
z  e.  ( X B y )  <->  z  e.  ( X B Y ) ) )
8682, 77, 853anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
( X  e/  (
y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) )  <-> 
( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )
8780, 84, 863orbi123d 1251 . . . . . . . . . . . . 13  |-  ( y  =  Y  ->  (
( ( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) )  <->  ( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) ) )
8874, 87imbi12d 311 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  (
( ( { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) )  ->  (
( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  (
y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )  <->  ( ( { X ,  Y , 
z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z
) )  ->  (
( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) ) ) )
89 eleq1 2343 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
y  e.  ( z B X )  <->  Y  e.  ( z B X ) ) )
9089, 71, 733anbi123d 1252 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
( y  e.  ( z B X )  /\  { X , 
y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z ) )  <->  ( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) ) )
9183, 90imbi12d 311 . . . . . . . . . . . . 13  |-  ( y  =  Y  ->  (
( y  e.  ( X B z )  ->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  <->  ( Y  e.  ( X B z )  ->  ( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) ) ) )
92 neleq1 2537 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
y  e/  l  <->  Y  e/  l ) )
93923anbi2d 1257 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  <->  ( X  e/  l  /\  Y  e/  l  /\  z  e/  l
) ) )
9463ineq1d 3369 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  Y  ->  (
( X B y )  i^i  l )  =  ( ( X B Y )  i^i  l ) )
9594eqeq1d 2291 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  Y  ->  (
( ( X B y )  i^i  l
)  =  (/)  <->  ( ( X B Y )  i^i  l )  =  (/) ) )
9675ineq1d 3369 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  Y  ->  (
( y B z )  i^i  l )  =  ( ( Y B z )  i^i  l ) )
9796eqeq1d 2291 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  Y  ->  (
( ( y B z )  i^i  l
)  =  (/)  <->  ( ( Y B z )  i^i  l )  =  (/) ) )
9895, 97anbi12d 691 . . . . . . . . . . . . . . . . 17  |-  ( y  =  Y  ->  (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  <->  ( (
( X B Y )  i^i  l )  =  (/)  /\  (
( Y B z )  i^i  l )  =  (/) ) ) )
9998imbi1d 308 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
( ( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) 
<->  ( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) )
10094neeq1d 2459 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  Y  ->  (
( ( X B y )  i^i  l
)  =/=  (/)  <->  ( ( X B Y )  i^i  l )  =/=  (/) ) )
10196neeq1d 2459 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  Y  ->  (
( ( y B z )  i^i  l
)  =/=  (/)  <->  ( ( Y B z )  i^i  l )  =/=  (/) ) )
102100, 101anbi12d 691 . . . . . . . . . . . . . . . . 17  |-  ( y  =  Y  ->  (
( ( ( X B y )  i^i  l )  =/=  (/)  /\  (
( y B z )  i^i  l )  =/=  (/) )  <->  ( (
( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) ) ) )
103102imbi1d 308 . . . . . . . . . . . . . . . 16  |-  ( y  =  Y  ->  (
( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  <->  ( (
( ( X B Y )  i^i  l
)  =/=  (/)  /\  (
( Y B z )  i^i  l )  =/=  (/) )  ->  (
( X B z )  i^i  l )  =  (/) ) ) )
10499, 103anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( y  =  Y  ->  (
( ( ( ( ( X B y )  i^i  l )  =  (/)  /\  (
( y B z )  i^i  l )  =  (/) )  ->  (
( X B z )  i^i  l )  =  (/) )  /\  (
( ( ( X B y )  i^i  l )  =/=  (/)  /\  (
( y B z )  i^i  l )  =/=  (/) )  ->  (
( X B z )  i^i  l )  =  (/) ) )  <->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) )
10593, 104imbi12d 311 . . . . . . . . . . . . . 14  |-  ( y  =  Y  ->  (
( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) )  <->  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) )
106105ralbidv 2563 . . . . . . . . . . . . 13  |-  ( y  =  Y  ->  ( A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) )  <->  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) )
10791, 106anbi12d 691 . . . . . . . . . . . 12  |-  ( y  =  Y  ->  (
( ( y  e.  ( X B z )  ->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) )  <->  ( ( Y  e.  ( X B z )  -> 
( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) ) )
10888, 107anbi12d 691 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
( ( ( { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) )  ->  (
( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  (
y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )  /\  ( ( y  e.  ( X B z )  ->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) )  <->  ( (
( { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  -> 
( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B z )  -> 
( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) ) ) )
109108ralbidv 2563 . . . . . . . . . 10  |-  ( y  =  Y  ->  ( A. z  e.  P  ( ( ( { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) )  ->  (
( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  (
y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )  /\  ( ( y  e.  ( X B z )  ->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) )  <->  A. z  e.  P  ( (
( { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  -> 
( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B z )  -> 
( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) ) ) )
11069, 109anbi12d 691 . . . . . . . . 9  |-  ( y  =  Y  ->  (
( ( X  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  ( a B y )  /\  b  e.  ( X B y )  /\  y  e.  ( X B c ) ) )  /\  A. z  e.  P  ( ( ( { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) )  ->  (
( X  e.  ( y B z )  /\  y  e/  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  (
y B z )  /\  y  e.  ( X B z )  /\  z  e/  ( X B y ) )  \/  ( X  e/  ( y B z )  /\  y  e/  ( X B z )  /\  z  e.  ( X B y ) ) ) )  /\  ( ( y  e.  ( X B z )  ->  ( y  e.  ( z B X )  /\  { X ,  y ,  z }  e.  C  /\  ( X  =/=  y  /\  X  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) ) )  <-> 
( ( X  =/= 
Y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  ( a B Y )  /\  b  e.  ( X B Y )  /\  Y  e.  ( X B c ) ) )  /\  A. z  e.  P  ( ( ( { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  -> 
( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B z )  -> 
( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) ) ) ) )
11159, 110rspc2v 2890 . . . . . . . 8  |-  ( ( X  e.  P  /\  Y  e.  P )  ->  ( A. x  e.  P  A. y  e.  P  ( ( x  =/=  y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( x  e.  ( a B y )  /\  b  e.  ( x B y )  /\  y  e.  ( x B c ) ) )  /\  A. z  e.  P  ( ( ( { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) )  ->  (
( x  e.  ( y B z )  /\  y  e/  (
x B z )  /\  z  e/  (
x B y ) )  \/  ( x  e/  ( y B z )  /\  y  e.  ( x B z )  /\  z  e/  ( x B y ) )  \/  (
x  e/  ( y B z )  /\  y  e/  ( x B z )  /\  z  e.  ( x B y ) ) ) )  /\  ( ( y  e.  ( x B z )  ->  (
y  e.  ( z B x )  /\  { x ,  y ,  z }  e.  C  /\  ( x  =/=  y  /\  x  =/=  z  /\  y  =/=  z
) ) )  /\  A. l  e.  L  ( ( x  e/  l  /\  y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( x B y )  i^i  l )  =  (/)  /\  ( ( y B z )  i^i  l
)  =  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( x B y )  i^i  l )  =/=  (/)  /\  ( ( y B z )  i^i  l )  =/=  (/) )  -> 
( ( x B z )  i^i  l
)  =  (/) ) ) ) ) ) )  ->  ( ( X  =/=  Y  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( X  e.  ( a B Y )  /\  b  e.  ( X B Y )  /\  Y  e.  ( X B c ) ) )  /\  A. z  e.  P  ( ( ( { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  -> 
( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B z )  -> 
( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) ) ) ) )
112 isibg2aa.7 . . . . . . . . . 10  |-  ( ph  ->  Z  e.  P )
113 tpeq3 3717 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  { X ,  Y ,  z }  =  { X ,  Y ,  Z }
)
114113eleq1d 2349 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  ( { X ,  Y , 
z }  e.  C  <->  { X ,  Y ,  Z }  e.  C
) )
115 neeq2 2455 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  ( X  =/=  z  <->  X  =/=  Z ) )
116 neeq2 2455 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  ( Y  =/=  z  <->  Y  =/=  Z ) )
117115, 1163anbi23d 1255 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  (
( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z
)  <->  ( X  =/= 
Y  /\  X  =/=  Z  /\  Y  =/=  Z
) ) )
118114, 117anbi12d 691 . . . . . . . . . . . . . 14  |-  ( z  =  Z  ->  (
( { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  <->  ( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) ) ) )
119 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  ( Y B z )  =  ( Y B Z ) )
120119eleq2d 2350 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  ( X  e.  ( Y B z )  <->  X  e.  ( Y B Z ) ) )
121 eqidd 2284 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  Y  =  Y )
122 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  ( X B z )  =  ( X B Z ) )
123121, 122neleq12d 24933 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  ( Y  e/  ( X B z )  <->  Y  e/  ( X B Z ) ) )
124 neleq1 2537 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  (
z  e/  ( X B Y )  <->  Z  e/  ( X B Y ) ) )
125120, 123, 1243anbi123d 1252 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  (
( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  <->  ( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) ) ) )
126 eqidd 2284 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  X  =  X )
127126, 119neleq12d 24933 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  ( X  e/  ( Y B z )  <->  X  e/  ( Y B Z ) ) )
128122eleq2d 2350 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  ( Y  e.  ( X B z )  <->  Y  e.  ( X B Z ) ) )
129127, 128, 1243anbi123d 1252 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  (
( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  <->  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) ) ) )
130 eleq1 2343 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  (
z  e.  ( X B Y )  <->  Z  e.  ( X B Y ) ) )
131127, 123, 1303anbi123d 1252 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  (
( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) )  <->  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) )
132125, 129, 1313orbi123d 1251 . . . . . . . . . . . . . 14  |-  ( z  =  Z  ->  (
( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) )  <-> 
( ( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) ) )
133118, 132imbi12d 311 . . . . . . . . . . . . 13  |-  ( z  =  Z  ->  (
( ( { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  -> 
( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  <->  ( ( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) )  ->  (
( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) ) ) )
134 oveq1 5865 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  (
z B X )  =  ( Z B X ) )
135134eleq2d 2350 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  ( Y  e.  ( z B X )  <->  Y  e.  ( Z B X ) ) )
136135, 114, 1173anbi123d 1252 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  (
( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  <->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/= 
Z ) ) ) )
137128, 136imbi12d 311 . . . . . . . . . . . . . 14  |-  ( z  =  Z  ->  (
( Y  e.  ( X B z )  ->  ( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  <-> 
( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/= 
Z ) ) ) ) )
138 neleq1 2537 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  (
z  e/  l  <->  Z  e/  l ) )
1391383anbi3d 1258 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  (
( X  e/  l  /\  Y  e/  l  /\  z  e/  l
)  <->  ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
) ) )
140119ineq1d 3369 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  Z  ->  (
( Y B z )  i^i  l )  =  ( ( Y B Z )  i^i  l ) )
141140eqeq1d 2291 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  Z  ->  (
( ( Y B z )  i^i  l
)  =  (/)  <->  ( ( Y B Z )  i^i  l )  =  (/) ) )
142141anbi2d 684 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  Z  ->  (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l
)  =  (/) )  <->  ( (
( X B Y )  i^i  l )  =  (/)  /\  (
( Y B Z )  i^i  l )  =  (/) ) ) )
143122ineq1d 3369 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  Z  ->  (
( X B z )  i^i  l )  =  ( ( X B Z )  i^i  l ) )
144143eqeq1d 2291 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  Z  ->  (
( ( X B z )  i^i  l
)  =  (/)  <->  ( ( X B Z )  i^i  l )  =  (/) ) )
145142, 144imbi12d 311 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) 
<->  ( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l )  =  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) ) ) )
146140neeq1d 2459 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  Z  ->  (
( ( Y B z )  i^i  l
)  =/=  (/)  <->  ( ( Y B Z )  i^i  l )  =/=  (/) ) )
147146anbi2d 684 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  Z  ->  (
( ( ( X B Y )  i^i  l )  =/=  (/)  /\  (
( Y B z )  i^i  l )  =/=  (/) )  <->  ( (
( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) ) ) )
148147, 144imbi12d 311 . . . . . . . . . . . . . . . . 17  |-  ( z  =  Z  ->  (
( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  <->  ( (
( ( X B Y )  i^i  l
)  =/=  (/)  /\  (
( Y B Z )  i^i  l )  =/=  (/) )  ->  (
( X B Z )  i^i  l )  =  (/) ) ) )
149145, 148anbi12d 691 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  (
( ( ( ( ( X B Y )  i^i  l )  =  (/)  /\  (
( Y B z )  i^i  l )  =  (/) )  ->  (
( X B z )  i^i  l )  =  (/) )  /\  (
( ( ( X B Y )  i^i  l )  =/=  (/)  /\  (
( Y B z )  i^i  l )  =/=  (/) )  ->  (
( X B z )  i^i  l )  =  (/) ) )  <->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) ) ) ) )
150139, 149imbi12d 311 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  (
( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) )  <->  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l )  =  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) ) ) ) ) )
151150ralbidv 2563 . . . . . . . . . . . . . 14  |-  ( z  =  Z  ->  ( A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) )  <->  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) ) ) ) ) )
152137, 151anbi12d 691 . . . . . . . . . . . . 13  |-  ( z  =  Z  ->  (
( ( Y  e.  ( X B z )  ->  ( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) )  <-> 
( ( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/= 
Z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l )  =  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) ) ) ) ) ) )
153133, 152anbi12d 691 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  (
( ( ( { X ,  Y , 
z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z
) )  ->  (
( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B z )  ->  ( Y  e.  ( z B X )  /\  { X ,  Y , 
z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) )  <->  ( (
( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/= 
Z ) )  -> 
( ( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B Z )  -> 
( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/= 
Z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l )  =  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) ) ) ) ) ) ) )
154153rspcv 2880 . . . . . . . . . . 11  |-  ( Z  e.  P  ->  ( A. z  e.  P  ( ( ( { X ,  Y , 
z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z
) )  ->  (
( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B z )  ->  ( Y  e.  ( z B X )  /\  { X ,  Y , 
z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l
)  =  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  -> 
( ( X B z )  i^i  l
)  =  (/) ) ) ) ) )  -> 
( ( ( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) )  ->  (
( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) ) ) ) ) ) ) )
155 isibg2aa.8 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  e.  L )
156 neleq2 2538 . . . . . . . . . . . . . . . . 17  |-  ( l  =  M  ->  ( X  e/  l  <->  X  e/  M ) )
157 neleq2 2538 . . . . . . . . . . . . . . . . 17  |-  ( l  =  M  ->  ( Y  e/  l  <->  Y  e/  M ) )
158 neleq2 2538 . . . . . . . . . . . . . . . . 17  |-  ( l  =  M  ->  ( Z  e/  l  <->  Z  e/  M ) )
159156, 157, 1583anbi123d 1252 . . . . . . . . . . . . . . . 16  |-  ( l  =  M  ->  (
( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
)  <->  ( X  e/  M  /\  Y  e/  M  /\  Z  e/  M ) ) )
160 ineq2 3364 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  M  ->  (
( X B Y )  i^i  l )  =  ( ( X B Y )  i^i 
M ) )
161160eqeq1d 2291 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  M  ->  (
( ( X B Y )  i^i  l
)  =  (/)  <->  ( ( X B Y )  i^i 
M )  =  (/) ) )
162 ineq2 3364 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  =  M  ->  (
( Y B Z )  i^i  l )  =  ( ( Y B Z )  i^i 
M ) )
163162eqeq1d 2291 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  M  ->  (
( ( Y B Z )  i^i  l
)  =  (/)  <->  ( ( Y B Z )  i^i 
M )  =  (/) ) )
164161, 163anbi12d 691 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  M  ->  (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  <->  ( (
( X B Y )  i^i  M )  =  (/)  /\  (
( Y B Z )  i^i  M )  =  (/) ) ) )
165 ineq2 3364 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  M  ->  (
( X B Z )  i^i  l )  =  ( ( X B Z )  i^i 
M ) )
166165eqeq1d 2291 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  M  ->  (
( ( X B Z )  i^i  l
)  =  (/)  <->  ( ( X B Z )  i^i 
M )  =  (/) ) )
167164, 166imbi12d 311 . . . . . . . . . . . . . . . . 17  |-  ( l  =  M  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l )  =  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) ) 
<->  ( ( ( ( X B Y )  i^i  M )  =  (/)  /\  ( ( Y B Z )  i^i 
M )  =  (/) )  ->  ( ( X B Z )  i^i 
M )  =  (/) ) ) )
168160neeq1d 2459 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  M  ->  (
( ( X B Y )  i^i  l
)  =/=  (/)  <->  ( ( X B Y )  i^i 
M )  =/=  (/) ) )
169162neeq1d 2459 . . . . . . . . . . . . . . . . . . 19  |-  ( l  =  M  ->  (
( ( Y B Z )  i^i  l
)  =/=  (/)  <->  ( ( Y B Z )  i^i 
M )  =/=  (/) ) )
170168, 169anbi12d 691 . . . . . . . . . . . . . . . . . 18  |-  ( l  =  M  ->  (
( ( ( X B Y )  i^i  l )  =/=  (/)  /\  (
( Y B Z )  i^i  l )  =/=  (/) )  <->  ( (
( X B Y )  i^i  M )  =/=  (/)  /\  ( ( Y B Z )  i^i  M )  =/=  (/) ) ) )
171170, 166imbi12d 311 . . . . . . . . . . . . . . . . 17  |-  ( l  =  M  ->  (
( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  <->  ( (
( ( X B Y )  i^i  M
)  =/=  (/)  /\  (
( Y B Z )  i^i  M )  =/=  (/) )  ->  (
( X B Z )  i^i  M )  =  (/) ) ) )
172167, 171anbi12d 691 . . . . . . . . . . . . . . . 16  |-  ( l  =  M  ->  (
( ( ( ( ( X B Y )  i^i  l )  =  (/)  /\  (
( Y B Z )  i^i  l )  =  (/) )  ->  (
( X B Z )  i^i  l )  =  (/) )  /\  (
( ( ( X B Y )  i^i  l )  =/=  (/)  /\  (
( Y B Z )  i^i  l )  =/=  (/) )  ->  (
( X B Z )  i^i  l )  =  (/) ) )  <->  ( (
( ( ( X B Y )  i^i 
M )  =  (/)  /\  ( ( Y B Z )  i^i  M
)  =  (/) )  -> 
( ( X B Z )  i^i  M
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  M )  =/=  (/)  /\  ( ( Y B Z )  i^i 
M )  =/=  (/) )  -> 
( ( X B Z )  i^i  M
)  =  (/) ) ) ) )
173159, 172imbi12d 311 . . . . . . . . . . . . . . 15  |-  ( l  =  M  ->  (
( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) ) ) )  <->  ( ( X  e/  M  /\  Y  e/  M  /\  Z  e/  M )  ->  (
( ( ( ( X B Y )  i^i  M )  =  (/)  /\  ( ( Y B Z )  i^i 
M )  =  (/) )  ->  ( ( X B Z )  i^i 
M )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  M )  =/=  (/)  /\  ( ( Y B Z )  i^i  M )  =/=  (/) )  ->  ( ( X B Z )  i^i  M )  =  (/) ) ) ) ) )
174173rspcv 2880 . . . . . . . . . . . . . 14  |-  ( M  e.  L  ->  ( A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) ) ) )  ->  ( ( X  e/  M  /\  Y  e/  M  /\  Z  e/  M )  ->  (
( ( ( ( X B Y )  i^i  M )  =  (/)  /\  ( ( Y B Z )  i^i 
M )  =  (/) )  ->  ( ( X B Z )  i^i 
M )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  M )  =/=  (/)  /\  ( ( Y B Z )  i^i  M )  =/=  (/) )  ->  ( ( X B Z )  i^i  M )  =  (/) ) ) ) ) )
175155, 174syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l )  =  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  ->  ( ( X B Z )  i^i  l )  =  (/) ) ) )  -> 
( ( X  e/  M  /\  Y  e/  M  /\  Z  e/  M )  ->  ( ( ( ( ( X B Y )  i^i  M
)  =  (/)  /\  (
( Y B Z )  i^i  M )  =  (/) )  ->  (
( X B Z )  i^i  M )  =  (/) )  /\  (
( ( ( X B Y )  i^i 
M )  =/=  (/)  /\  (
( Y B Z )  i^i  M )  =/=  (/) )  ->  (
( X B Z )  i^i  M )  =  (/) ) ) ) ) )
176175anim2d 548 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) ) ) ) )  ->  (
( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/= 
Z ) ) )  /\  ( ( X  e/  M  /\  Y  e/  M  /\  Z  e/  M )  ->  (
( ( ( ( X B Y )  i^i  M )  =  (/)  /\  ( ( Y B Z )  i^i 
M )  =  (/) )  ->  ( ( X B Z )  i^i 
M )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  M )  =/=  (/)  /\  ( ( Y B Z )  i^i  M )  =/=  (/) )  ->  ( ( X B Z )  i^i  M )  =  (/) ) ) ) ) ) )
177176anim2d 548 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) )  ->  (
( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  Z  e/  l
)  ->  ( (
( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B Z )  i^i  l
)  =  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B Z )  i^i  l )  =/=  (/) )  -> 
( ( X B Z )  i^i  l
)  =  (/) ) ) ) ) )  -> 
( ( ( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) )  ->  (
( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B Z )  ->  ( Y  e.  ( Z B X )  /\  { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/=  Z
) ) )  /\  ( ( X  e/  M  /\  Y  e/  M  /\  Z  e/  M )  ->  ( ( ( ( ( X B Y )  i^i  M
)  =  (/)  /\  (
( Y B Z )  i^i  M )  =  (/) )  ->  (
( X B Z )  i^i  M )  =  (/) )  /\  (
( ( ( X B Y )  i^i 
M )  =/=  (/)  /\  (
( Y B Z )  i^i  M )  =/=  (/) )  ->  (
( X B Z )  i^i  M )  =  (/) ) ) ) ) ) ) )
178154, 177syl9 66 . . . . . . . . . 10  |-  ( Z  e.  P  ->  ( ph  ->  ( A. z  e.  P  ( (
( { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) )  -> 
( ( X  e.  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e.  ( X B z )  /\  z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B z )  /\  Y  e/  ( X B z )  /\  z  e.  ( X B Y ) ) ) )  /\  ( ( Y  e.  ( X B z )  -> 
( Y  e.  ( z B X )  /\  { X ,  Y ,  z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  z  /\  Y  =/=  z ) ) )  /\  A. l  e.  L  ( ( X  e/  l  /\  Y  e/  l  /\  z  e/  l )  ->  (
( ( ( ( X B Y )  i^i  l )  =  (/)  /\  ( ( Y B z )  i^i  l )  =  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) )  /\  ( ( ( ( X B Y )  i^i  l )  =/=  (/)  /\  ( ( Y B z )  i^i  l )  =/=  (/) )  ->  ( ( X B z )  i^i  l )  =  (/) ) ) ) ) )  ->  ( (
( { X ,  Y ,  Z }  e.  C  /\  ( X  =/=  Y  /\  X  =/=  Z  /\  Y  =/= 
Z ) )  -> 
( ( X  e.  ( Y B Z )  /\  Y  e/  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y B Z )  /\  Y  e.  ( X B Z )  /\  Z  e/  ( X B Y ) )  \/  ( X  e/  ( Y