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

Theorem isibg2 26110
Description: The predicate "is an incidence-betweenness geometry".

B-1 If  q is between  p and  r then it is between  r and  p and  p,  q,  r are collinear and distinct.

B-2 If  p and  q are distinct, then there are points  a,  b,  c such that  a is before  p and  q,  b is between  p and  q,  c is after  p and  q.

B-3 If three points  p,  q,  r are collinear and distinct then exactly one of the followings occurs:  p is between  q and  r,  q is between  p and  r,  r is between  p and  q.

B-4 "Being on the same side" is a transitive relation. If  p and  q are not on the same side of  l and  q and  r are not on the same side of  l then  p and  r are on the same side of  l. (For my private use only. Don't use.) (Contributed by FL, 1-Apr-2016.)

Hypotheses
Ref Expression
isibg.1  |-  P  =  (PPoints `  G )
isibg.2  |-  L  =  (PLines `  G )
isibg.3  |-  B  =  (btw `  G )
isibg.6  |-  C  =  (coln `  G )
Assertion
Ref Expression
isibg2  |-  ( G  e. Ibg 
<->  ( G  e. Ig  /\  A. p  e.  P  A. q  e.  P  (
( p  =/=  q  ->  E. a  e.  P  E. b  e.  P  E. c  e.  P  ( p  e.  (
a B q )  /\  b  e.  ( p B q )  /\  q  e.  ( p B c ) ) )  /\  A. r  e.  P  (
( ( { p ,  q ,  r }  e.  C  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q B r )  /\  q  e/  (
p B r )  /\  r  e/  (
p B q ) )  \/  ( p  e/  ( q B r )  /\  q  e.  ( p B r )  /\  r  e/  ( p B q ) )  \/  (
p  e/  ( q B r )  /\  q  e/  ( p B r )  /\  r  e.  ( p B q ) ) ) )  /\  ( ( q  e.  ( p B r )  ->  (
q  e.  ( r B p )  /\  { p ,  q ,  r }  e.  C  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  L  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p B q )  i^i  l )  =  (/)  /\  ( ( q B r )  i^i  l
)  =  (/) )  -> 
( ( p B r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p B q )  i^i  l )  =/=  (/)  /\  ( ( q B r )  i^i  l )  =/=  (/) )  -> 
( ( p B r )  i^i  l
)  =  (/) ) ) ) ) ) ) ) )
Distinct variable groups:    a, b,
c, l, p, q, r, B    P, a,
b, c, p, q, r    C, p, q, r    L, l, p, q, r
Allowed substitution hints:    C( a, b, c, l)    P( l)    G( r, q, p, a, b, c, l)    L( a, b, c)

Proof of Theorem isibg2
Dummy variables  d 
e  f  g  h are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5525 . . . . . 6  |-  ( f  =  G  ->  (PPoints `  f )  =  (PPoints `  G ) )
2 fveq2 5525 . . . . . . 7  |-  ( f  =  G  ->  (PLines `  f )  =  (PLines `  G ) )
3 dfsbcq 2993 . . . . . . 7  |-  ( (PLines `  f )  =  (PLines `  G )  ->  ( [. (PLines `  f )  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (PLines `  G )  /  h ]. [. (coln `  f
)  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
42, 3syl 15 . . . . . 6  |-  ( f  =  G  ->  ( [. (PLines `  f )  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (PLines `  G )  /  h ]. [. (coln `  f
)  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
51, 4sbcbidv2 24969 . . . . 5  |-  ( f  =  G  ->  ( [. (PPoints `  f )  /  g ]. [. (PLines `  f )  /  h ]. [. (coln `  f
)  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (PPoints `  G
)  /  g ]. [. (PLines `  G )  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
6 fveq2 5525 . . . . . . . 8  |-  ( f  =  G  ->  (coln `  f )  =  (coln `  G ) )
7 fveq2 5525 . . . . . . . . 9  |-  ( f  =  G  ->  (btw `  f )  =  (btw
`  G ) )
8 dfsbcq 2993 . . . . . . . . 9  |-  ( (btw
`  f )  =  (btw `  G )  ->  ( [. (btw `  f )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
97, 8syl 15 . . . . . . . 8  |-  ( f  =  G  ->  ( [. (btw `  f )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
106, 9sbcbidv2 24969 . . . . . . 7  |-  ( f  =  G  ->  ( [. (coln `  f )  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
1110sbcbidv 3045 . . . . . 6  |-  ( f  =  G  ->  ( [. (PLines `  G )  /  h ]. [. (coln `  f )  /  d ]. [. (btw `  f
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (PLines `  G )  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
1211sbcbidv 3045 . . . . 5  |-  ( f  =  G  ->  ( [. (PPoints `  G )  /  g ]. [. (PLines `  G )  /  h ]. [. (coln `  f
)  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (PPoints `  G
)  /  g ]. [. (PLines `  G )  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
135, 12bitrd 244 . . . 4  |-  ( f  =  G  ->  ( [. (PPoints `  f )  /  g ]. [. (PLines `  f )  /  h ]. [. (coln `  f
)  /  d ]. [. (btw `  f )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. (PPoints `  G
)  /  g ]. [. (PLines `  G )  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
14 isibg.1 . . . . . . 7  |-  P  =  (PPoints `  G )
1514eqcomi 2287 . . . . . 6  |-  (PPoints `  G
)  =  P
16 dfsbcq 2993 . . . . . 6  |-  ( (PPoints `  G )  =  P  ->  ( [. (PPoints `  G )  /  g ]. [. (PLines `  G
)  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. P  / 
g ]. [. (PLines `  G )  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
1715, 16ax-mp 8 . . . . 5  |-  ( [. (PPoints `  G )  / 
g ]. [. (PLines `  G )  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. P  / 
g ]. [. (PLines `  G )  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
18 fvex 5539 . . . . . . . 8  |-  (PPoints `  G
)  e.  _V
1914, 18eqeltri 2353 . . . . . . 7  |-  P  e. 
_V
20 isibg.2 . . . . . . . . . 10  |-  L  =  (PLines `  G )
2120eqcomi 2287 . . . . . . . . 9  |-  (PLines `  G )  =  L
22 dfsbcq 2993 . . . . . . . . 9  |-  ( (PLines `  G )  =  L  ->  ( [. (PLines `  G )  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. L  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
2321, 22ax-mp 8 . . . . . . . 8  |-  ( [. (PLines `  G )  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. L  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
2423sbcbiiOLD 3047 . . . . . . 7  |-  ( P  e.  _V  ->  ( [. P  /  g ]. [. (PLines `  G
)  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. P  / 
g ]. [. L  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
2519, 24ax-mp 8 . . . . . 6  |-  ( [. P  /  g ]. [. (PLines `  G )  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. P  / 
g ]. [. L  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
26 fvex 5539 . . . . . . . . . 10  |-  (PLines `  G )  e.  _V
2720, 26eqeltri 2353 . . . . . . . . 9  |-  L  e. 
_V
28 isibg.6 . . . . . . . . . . . . 13  |-  C  =  (coln `  G )
2928eqcomi 2287 . . . . . . . . . . . 12  |-  (coln `  G )  =  C
30 dfsbcq 2993 . . . . . . . . . . . 12  |-  ( (coln `  G )  =  C  ->  ( [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. C  / 
d ]. [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
3129, 30ax-mp 8 . . . . . . . . . . 11  |-  ( [. (coln `  G )  / 
d ]. [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. C  / 
d ]. [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
32 fvex 5539 . . . . . . . . . . . . 13  |-  (coln `  G )  e.  _V
3328, 32eqeltri 2353 . . . . . . . . . . . 12  |-  C  e. 
_V
34 isibg.3 . . . . . . . . . . . . . . 15  |-  B  =  (btw `  G )
3534eqcomi 2287 . . . . . . . . . . . . . 14  |-  (btw `  G )  =  B
36 dfsbcq 2993 . . . . . . . . . . . . . 14  |-  ( (btw
`  G )  =  B  ->  ( [. (btw `  G )  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
3735, 36ax-mp 8 . . . . . . . . . . . . 13  |-  ( [. (btw `  G )  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
3837sbcbiiOLD 3047 . . . . . . . . . . . 12  |-  ( C  e.  _V  ->  ( [. C  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. C  / 
d ]. [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
3933, 38ax-mp 8 . . . . . . . . . . 11  |-  ( [. C  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. C  / 
d ]. [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
4031, 39bitri 240 . . . . . . . . . 10  |-  ( [. (coln `  G )  / 
d ]. [. (btw `  G )  /  e ]. A. p  e.  g 
A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. C  / 
d ]. [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
4140sbcbiiOLD 3047 . . . . . . . . 9  |-  ( L  e.  _V  ->  ( [. L  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. L  /  h ]. [. C  / 
d ]. [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
4227, 41ax-mp 8 . . . . . . . 8  |-  ( [. L  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. L  /  h ]. [. C  / 
d ]. [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) )
4342sbcbiiOLD 3047 . . . . . . 7  |-  ( P  e.  _V  ->  ( [. P  /  g ]. [. L  /  h ]. [. (coln `  G
)  /  d ]. [. (btw `  G )  /  e ]. A. p  e.  g  A. q  e.  g  (
( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  (
( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. P  / 
g ]. [. L  /  h ]. [. C  / 
d ]. [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) ) ) )
4419, 43ax-mp 8 . . . . . 6  |-  ( [. P  /  g ]. [. L  /  h ]. [. (coln `  G )  /  d ]. [. (btw `  G
)  /  e ]. A. p  e.  g  A. q  e.  g 
( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )  /\  b  e.  ( p e q )  /\  q  e.  ( p e c ) ) )  /\  A. r  e.  g  ( ( ( { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) )  ->  (
( p  e.  ( q e r )  /\  q  e/  (
p e r )  /\  r  e/  (
p e q ) )  \/  ( p  e/  ( q e r )  /\  q  e.  ( p e r )  /\  r  e/  ( p e q ) )  \/  (
p  e/  ( q
e r )  /\  q  e/  ( p e r )  /\  r  e.  ( p e q ) ) ) )  /\  ( q  e.  ( p e r )  ->  ( q  e.  ( r e p )  /\  { p ,  q ,  r }  e.  d  /\  ( p  =/=  q  /\  p  =/=  r  /\  q  =/=  r
) ) )  /\  A. l  e.  h  ( ( p  e/  l  /\  q  e/  l  /\  r  e/  l
)  ->  ( (
( ( ( p e q )  i^i  l )  =  (/)  /\  ( ( q e r )  i^i  l
)  =  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) )  /\  ( ( ( ( p e q )  i^i  l )  =/=  (/)  /\  ( ( q e r )  i^i  l )  =/=  (/) )  -> 
( ( p e r )  i^i  l
)  =  (/) ) ) ) ) )  <->  [. P  / 
g ]. [. L  /  h ]. [. C  / 
d ]. [. B  / 
e ]. A. p  e.  g  A. q  e.  g  ( ( p  =/=  q  ->  E. a  e.  g  E. b  e.  g  E. c  e.  g  ( p  e.  ( a e q )