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

Theorem isibcg 26191
Description: The predicate "is a incidence betwenness geometry with congruences". (For my private use only. Don't use.) (Contributed by FL, 16-Sep-2016.)
Hypotheses
Ref Expression
isibcg.1  |-  .~  a  =  (angc `  G )
isibcg.2  |-  P  =  (PPoints `  G )
isibcg.3  |-  U  =  (Segments `  G )
isibcg.4  |-  B  =  (btw `  G )
isibcg.5  |-  R  =  (ray `  G )
isibcg.6  |-  .~  s  =  (segc `  G )
isibcg.7  |-  S  =  ( seg `  G
)
isibcg.8  |-  L  =  ( line `  G
)
isibcg.9  |-  H  =  (Halfplane `  G )
isibcg.10  |-  T  =  (triangle `  G )
isibcg.11  |-  A  =  (angle `  G )
isibcg.12  |-  .~  t  =  (trcng `  G )
isibcg.13  |-  W  =  ( PdWords 3 )
Assertion
Ref Expression
isibcg  |-  ( G  e. Ibcg 
<->  ( G  e. Ibg  /\  (  .~  s  Er  U  /\  .~  a  Er  ( A " W ) )  /\  A. d  e.  P  A. e  e.  P  ( d  =/=  e  ->  ( A. a  e.  P  A. b  e.  P  (
( a  =/=  b  ->  E! f  e.  ( d R e ) ( f  =/=  d  /\  ( a S b )  .~  s ( d S f ) ) )  /\  A. c  e.  P  (
( c  e.  ( a B b )  /\  ( a S b )  .~  s
( d S e ) )  ->  E. f  e.  P  ( f  e.  ( d B e )  /\  ( a S c )  .~  s ( d S f )  /\  (
c S b )  .~  s ( f S e ) ) ) )  /\  A. a  e.  W  ( A. b  e.  ( H `  ( d L e ) ) E! f  e.  b  ( A `  a
)  .~  a ( A `  <" e
d f "> )  /\  ( ( ( a `  1 ) S ( a ` 
2 ) )  .~  s ( d S e )  ->  A. b  e.  ( H `  (
d L e ) ) E. f  e.  b  a  .~  t
( T `  <" d e f "> ) ) ) ) ) ) )
Distinct variable groups:    a, b,
c, d, e, f   
a,  .~  a, b,
d, e, f    a,  .~  s, b, c, d, e, f    a,  .~  t, b, d, e, f    A, a, b, c, d, e, f    B, a, b, c, d, e, f    H, a, b, d, e, f    L, a, b, c, d, e, f    P, a, b, c, d, e, f    R, a, b, c, d, e, f    S, a, b, c, d, e, f    T, a, b, d, e, f    U, a, b, d, e, f    W, a, b, d, e, f
Allowed substitution hints:    T( c)    U( c)    G( e, f, a, b, c, d)    H( c)    W( c)    .~  a( c)    .~  t( c)

Proof of Theorem isibcg
Dummy variables  g 
l  o  p  q  r  s  t  u  v  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ibcg 26190 . . 3  |- Ibcg  =  {
g  e. Ibg  |  [. (angc `  g )  /  o ]. [. (PPoints `  g
)  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) }
21eleq2i 2347 . 2  |-  ( G  e. Ibcg 
<->  G  e.  { g  e. Ibg  |  [. (angc `  g )  /  o ]. [. (PPoints `  g
)  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) } )
3 fveq2 5525 . . . 4  |-  ( g  =  G  ->  (angc `  g )  =  (angc `  G ) )
4 fveq2 5525 . . . . 5  |-  ( g  =  G  ->  (PPoints `  g )  =  (PPoints `  G ) )
5 fveq2 5525 . . . . . 6  |-  ( g  =  G  ->  (btw `  g )  =  (btw
`  G ) )
6 fveq2 5525 . . . . . . 7  |-  ( g  =  G  ->  (ray `  g )  =  (ray
`  G ) )
7 fveq2 5525 . . . . . . . 8  |-  ( g  =  G  ->  (segc `  g )  =  (segc `  G ) )
8 fveq2 5525 . . . . . . . . 9  |-  ( g  =  G  ->  ( seg `  g )  =  ( seg `  G
) )
9 fveq2 5525 . . . . . . . . . 10  |-  ( g  =  G  ->  ( line `  g )  =  ( line `  G
) )
10 fveq2 5525 . . . . . . . . . . 11  |-  ( g  =  G  ->  (angle `  g )  =  (angle `  G ) )
11 fveq2 5525 . . . . . . . . . . . 12  |-  ( g  =  G  ->  (triangle `  g )  =  (triangle `  G ) )
12 fveq2 5525 . . . . . . . . . . . . . 14  |-  ( g  =  G  ->  (Halfplane `  g )  =  (Halfplane `  G ) )
13 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( g  =  G  ->  (Segments `  g )  =  (Segments `  G ) )
14 fveq2 5525 . . . . . . . . . . . . . . . 16  |-  ( g  =  G  ->  (trcng `  g )  =  (trcng `  G ) )
15 biidd 228 . . . . . . . . . . . . . . . 16  |-  ( g  =  G  ->  (
( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  ( s  Er  y  /\  o  Er  ( u " w
)  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
1614, 15sbcbidv2 24969 . . . . . . . . . . . . . . 15  |-  ( g  =  G  ->  ( [. (trcng `  g )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
1713, 16sbcbidv2 24969 . . . . . . . . . . . . . 14  |-  ( g  =  G  ->  ( [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (Segments `  G
)  /  y ]. [. (trcng `  G )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
1812, 17sbcbidv2 24969 . . . . . . . . . . . . 13  |-  ( g  =  G  ->  ( [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
1918sbcbidv 3045 . . . . . . . . . . . 12  |-  ( g  =  G  ->  ( [. ( pdWords 3 )  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g
)  /  y ]. [. (trcng `  g )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
2011, 19sbcbidv2 24969 . . . . . . . . . . 11  |-  ( g  =  G  ->  ( [. (triangle `  g )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  g
)  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (triangle `  G
)  /  v ]. [. ( pdWords 3 )  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G
)  /  y ]. [. (trcng `  G )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
2110, 20sbcbidv2 24969 . . . . . . . . . 10  |-  ( g  =  G  ->  ( [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (angle `  G
)  /  u ]. [. (triangle `  G )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
229, 21sbcbidv2 24969 . . . . . . . . 9  |-  ( g  =  G  ->  ( [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
238, 22sbcbidv2 24969 . . . . . . . 8  |-  ( g  =  G  ->  ( [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
247, 23sbcbidv2 24969 . . . . . . 7  |-  ( g  =  G  ->  ( [. (segc `  g )  /  s ]. [. ( seg `  g )  / 
t ]. [. ( line `  g )  /  l ]. [. (angle `  g
)  /  u ]. [. (triangle `  g )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  g
)  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (segc `  G
)  /  s ]. [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
256, 24sbcbidv2 24969 . . . . . 6  |-  ( g  =  G  ->  ( [. (ray `  g )  /  r ]. [. (segc `  g )  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (ray `  G
)  /  r ]. [. (segc `  G )  /  s ]. [. ( seg `  G )  / 
t ]. [. ( line `  G )  /  l ]. [. (angle `  G
)  /  u ]. [. (triangle `  G )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
265, 25sbcbidv2 24969 . . . . 5  |-  ( g  =  G  ->  ( [. (btw `  g )  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g
)  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (btw `  G
)  /  q ]. [. (ray `  G )  /  r ]. [. (segc `  G )  /  s ]. [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
274, 26sbcbidv2 24969 . . . 4  |-  ( g  =  G  ->  ( [. (PPoints `  g )  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g
)  /  r ]. [. (segc `  g )  /  s ]. [. ( seg `  g )  / 
t ]. [. ( line `  g )  /  l ]. [. (angle `  g
)  /  u ]. [. (triangle `  g )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  g
)  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (PPoints `  G
)  /  p ]. [. (btw `  G )  /  q ]. [. (ray `  G )  /  r ]. [. (segc `  G
)  /  s ]. [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
283, 27sbcbidv2 24969 . . 3  |-  ( g  =  G  ->  ( [. (angc `  g )  /  o ]. [. (PPoints `  g )  /  p ]. [. (btw `  g
)  /  q ]. [. (ray `  g )  /  r ]. [. (segc `  g )  /  s ]. [. ( seg `  g
)  /  t ]. [. ( line `  g
)  /  l ]. [. (angle `  g )  /  u ]. [. (triangle `  g )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  g )  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (angc `  G
)  /  o ]. [. (PPoints `  G )  /  p ]. [. (btw `  G )  /  q ]. [. (ray `  G
)  /  r ]. [. (segc `  G )  /  s ]. [. ( seg `  G )  / 
t ]. [. ( line `  G )  /  l ]. [. (angle `  G
)  /  u ]. [. (triangle `  G )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
2928elrab 2923 . 2  |-  ( G  e.  { g  e. Ibg 
|  [. (angc `  g
)  /  o ]. [. (PPoints `  g )  /  p ]. [. (btw `  g )  /  q ]. [. (ray `  g
)  /  r ]. [. (segc `  g )  /  s ]. [. ( seg `  g )  / 
t ]. [. ( line `  g )  /  l ]. [. (angle `  g
)  /  u ]. [. (triangle `  g )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  g
)  /  x ]. [. (Segments `  g )  /  y ]. [. (trcng `  g )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) }  <->  ( G  e. Ibg  /\  [. (angc `  G )  /  o ]. [. (PPoints `  G
)  /  p ]. [. (btw `  G )  /  q ]. [. (ray `  G )  /  r ]. [. (segc `  G
)  /  s ]. [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) ) ) )
30 fvex 5539 . . . . . 6  |-  (angc `  G )  e.  _V
31 isibcg.1 . . . . . . 7  |-  .~  a  =  (angc `  G )
32 eqtr 2300 . . . . . . . . . 10  |-  ( ( o  =  (angc `  G )  /\  (angc `  G )  =  .~  a )  ->  o  =  .~  a )
33 ereq1 6667 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( o  =  .~  a  -> 
( o  Er  (
u " w )  <->  .~  a  Er  (
u " w ) ) )
34 breq 4025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( o  =  .~  a  -> 
( ( u `  a ) o ( u `  <" e
d f "> ) 
<->  ( u `  a
)  .~  a (
u `  <" e
d f "> ) ) )
3534reubidv 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( o  =  .~  a  -> 
( E! f  e.  b  ( u `  a ) o ( u `  <" e
d f "> ) 
<->  E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> ) ) )
3635ralbidv 2563 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( o  =  .~  a  -> 
( A. b  e.  ( x `  (
d l e ) ) E! f  e.  b  ( u `  a ) o ( u `  <" e
d f "> ) 
<-> 
A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> ) ) )
3736anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( o  =  .~  a  -> 
( ( A. b  e.  ( x `  (
d l e ) ) E! f  e.  b  ( u `  a ) o ( u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) )  <->  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `
 a )  .~  a ( u `  <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) )
3837ralbidv 2563 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( o  =  .~  a  -> 
( A. a  e.  w  ( A. b  e.  ( x `  (
d l e ) ) E! f  e.  b  ( u `  a ) o ( u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) )  <->  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `
 a )  .~  a ( u `  <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) )
3938anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( o  =  .~  a  -> 
( ( A. a  e.  p  A. b  e.  p  ( (
a  =/=  b  ->  E! f  e.  (
d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) )  <->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) )
4039imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( o  =  .~  a  -> 
( ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) )  <-> 
( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) )
41402ralbidv 2585 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( o  =  .~  a  -> 
( A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) )  <->  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) )
4233, 413anbi23d 1255 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( o  =  .~  a  -> 
( ( s  Er  y  /\  o  Er  ( u " w
)  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  ( s  Er  y  /\  .~  a  Er  ( u " w
)  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
4342sbcbidv 3045 . . . . . . . . . . . . . . . . . . . . 21  |-  ( o  =  .~  a  -> 
( [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  .~  a  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
4443sbcbidv 3045 . . . . . . . . . . . . . . . . . . . 20  |-  ( o  =  .~  a  -> 
( [. (Segments `  G
)  /  y ]. [. (trcng `  G )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (Segments `  G
)  /  y ]. [. (trcng `  G )  /  z ]. (
s  Er  y  /\  .~  a  Er  ( u
" w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
4544sbcbidv 3045 . . . . . . . . . . . . . . . . . . 19  |-  ( o  =  .~  a  -> 
( [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  .~  a  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
4645sbcbidv 3045 . . . . . . . . . . . . . . . . . 18  |-  ( o  =  .~  a  -> 
( [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  .~  a  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
4746sbcbidv 3045 . . . . . . . . . . . . . . . . 17  |-  ( o  =  .~  a  -> 
( [. (triangle `  G
)  /  v ]. [. ( pdWords 3 )  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G
)  /  y ]. [. (trcng `  G )  /  z ]. (
s  Er  y  /\  o  Er  ( u " w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (triangle `  G
)  /  v ]. [. ( pdWords 3 )  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G
)  /  y ]. [. (trcng `  G )  /  z ]. (
s  Er  y  /\  .~  a  Er  ( u
" w )  /\  A. d  e.  p  A. e  e.  p  (
d  =/=  e  -> 
( A. a  e.  p  A. b  e.  p  ( ( a  =/=  b  ->  E! f  e.  ( d
r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
4847sbcbidv 3045 . . . . . . . . . . . . . . . 16  |-  ( o  =  .~  a  -> 
( [. (angle `  G
)  /  u ]. [. (triangle `  G )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (angle `  G
)  /  u ]. [. (triangle `  G )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  .~  a  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
4948sbcbidv 3045 . . . . . . . . . . . . . . 15  |-  ( o  =  .~  a  -> 
( [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  .~  a  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
5049sbcbidv 3045 . . . . . . . . . . . . . 14  |-  ( o  =  .~  a  -> 
( [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  .~  a  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
5150sbcbidv 3045 . . . . . . . . . . . . 13  |-  ( o  =  .~  a  -> 
( [. (segc `  G
)  /  s ]. [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (segc `  G
)  /  s ]. [. ( seg `  G
)  /  t ]. [. ( line `  G
)  /  l ]. [. (angle `  G )  /  u ]. [. (triangle `  G )  /  v ]. [. ( pdWords 3
)  /  w ]. [. (Halfplane `  G )  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G
)  /  z ]. ( s  Er  y  /\  .~  a  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
)  .~  a (
u `  <" e
d f "> )  /\  ( ( ( a `  1 ) t ( a ` 
2 ) ) s ( d t e )  ->  A. b  e.  ( x `  (
d l e ) ) E. f  e.  b  a z ( v `  <" d
e f "> ) ) ) ) ) ) ) )
5251sbcbidv 3045 . . . . . . . . . . . 12  |-  ( o  =  .~  a  -> 
( [. (ray `  G
)  /  r ]. [. (segc `  G )  /  s ]. [. ( seg `  G )  / 
t ]. [. ( line `  G )  /  l ]. [. (angle `  G
)  /  u ]. [. (triangle `  G )  /  v ]. [. (
pdWords 3 )  /  w ]. [. (Halfplane `  G
)  /  x ]. [. (Segments `  G )  /  y ]. [. (trcng `  G )  /  z ]. ( s  Er  y  /\  o  Er  (
u " w )  /\  A. d  e.  p  A. e  e.  p  ( d  =/=  e  ->  ( A. a  e.  p  A. b  e.  p  (
( a  =/=  b  ->  E! f  e.  ( d r e ) ( f  =/=  d  /\  ( a t b ) s ( d t f ) ) )  /\  A. c  e.  p  ( (
c  e.  ( a q b )  /\  ( a t b ) s ( d t e ) )  ->  E. f  e.  p  ( f  e.  ( d q e )  /\  ( a t c ) s ( d t f )  /\  ( c t b ) s ( f t e ) ) ) )  /\  A. a  e.  w  ( A. b  e.  ( x `  ( d l e ) ) E! f  e.  b  ( u `  a
) o ( u `
 <" e d f "> )  /\  ( ( ( a `
 1 ) t ( a `  2
) ) s ( d t e )  ->  A. b  e.  ( x `  ( d l e ) ) E. f  e.  b  a z ( v `
 <" d e f "> )
) ) ) ) )  <->  [. (ray `  G
)  /  r ]. [. (segc `  G )  /  s ]. [. ( seg `  G )  / 
t ]. [. ( line `  G )  /  l ]. [. (angle `  G
)  /  u ]. [. (triangle `  G )  /  v ]. [.