Step | Hyp | Ref
| Expression |
1 | | trgcopy.p |
. . . . . . 7
     |
2 | | trgcopy.m |
. . . . . . 7
     |
3 | | eqid 2461 |
. . . . . . 7
cgrG  cgrG   |
4 | | trgcopy.g |
. . . . . . . . . . 11

TarskiG |
5 | 4 | ad2antrr 737 |
. . . . . . . . . 10
             ⟂G        TarskiG |
6 | 5 | ad2antrr 737 |
. . . . . . . . 9
               ⟂G       
        cgrG          TarskiG |
7 | 6 | ad2antrr 737 |
. . . . . . . 8
                 ⟂G        
       cgrG         
       ⟂G         hpG            TarskiG |
8 | 7 | adantr 471 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                          
TarskiG |
9 | | trgcopy.a |
. . . . . . . . . 10
   |
10 | 9 | ad2antrr 737 |
. . . . . . . . 9
             ⟂G          |
11 | 10 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
        cgrG            |
12 | 11 | ad3antrrr 741 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                          
  |
13 | | trgcopy.b |
. . . . . . . . . 10
   |
14 | 13 | ad2antrr 737 |
. . . . . . . . 9
             ⟂G          |
15 | 14 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
        cgrG            |
16 | 15 | ad3antrrr 741 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                          
  |
17 | | trgcopy.c |
. . . . . . . . 9
   |
18 | 17 | ad6antr 747 |
. . . . . . . 8
                 ⟂G        
       cgrG         
       ⟂G         hpG              |
19 | 18 | adantr 471 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                          
  |
20 | | trgcopy.d |
. . . . . . . . . 10
   |
21 | 20 | ad2antrr 737 |
. . . . . . . . 9
             ⟂G          |
22 | 21 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
        cgrG            |
23 | 22 | ad3antrrr 741 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                          
  |
24 | | trgcopy.e |
. . . . . . . . . 10
   |
25 | 24 | ad2antrr 737 |
. . . . . . . . 9
             ⟂G          |
26 | 25 | ad2antrr 737 |
. . . . . . . 8
               ⟂G       
        cgrG            |
27 | 26 | ad3antrrr 741 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                          
  |
28 | | simprl 769 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
29 | | trgcopy.3 |
. . . . . . . . 9
       |
30 | 29 | ad2antrr 737 |
. . . . . . . 8
             ⟂G              |
31 | 30 | ad5antr 745 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
32 | | trgcopy.i |
. . . . . . . 8
Itv   |
33 | | trgcopy.l |
. . . . . . . . . . 11
LineG   |
34 | | trgcopy.1 |
. . . . . . . . . . 11
         |
35 | 1, 33, 32, 4, 13, 17, 9, 34 | ncoltgdim2 24658 |
. . . . . . . . . 10
 DimTarskiG≥  |
36 | 35 | ad4antr 743 |
. . . . . . . . 9
               ⟂G       
        cgrG          DimTarskiG≥  |
37 | 36 | ad3antrrr 741 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                           DimTarskiG≥  |
38 | 1, 32, 33, 4, 9, 13, 17, 34 | ncolne1 24718 |
. . . . . . . . . . . . . 14
   |
39 | 1, 32, 33, 4, 9, 13, 38 | tgelrnln 24723 |
. . . . . . . . . . . . 13
       |
40 | 39 | ad2antrr 737 |
. . . . . . . . . . . 12
             ⟂G              |
41 | | simplr 767 |
. . . . . . . . . . . 12
             ⟂G              |
42 | 1, 33, 32, 5, 40, 41 | tglnpt 24642 |
. . . . . . . . . . 11
             ⟂G          |
43 | 42 | ad2antrr 737 |
. . . . . . . . . 10
               ⟂G       
        cgrG            |
44 | 43 | ad2antrr 737 |
. . . . . . . . 9
                 ⟂G        
       cgrG         
       ⟂G         hpG              |
45 | 44 | adantr 471 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                          
  |
46 | | simplr 767 |
. . . . . . . . . 10
               ⟂G       
        cgrG            |
47 | 46 | ad2antrr 737 |
. . . . . . . . 9
                 ⟂G        
       cgrG         
       ⟂G         hpG              |
48 | 47 | adantr 471 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
49 | 41 | ad5antr 745 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                          
      |
50 | 38 | ad7antr 749 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
51 | 1, 32, 33, 8, 12, 16, 50 | tglinecom 24728 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                     |
52 | 49, 51 | eleqtrd 2541 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                          
      |
53 | | simp-6r 786 |
. . . . . . . . . . . 12
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
54 | 33, 8, 53 | perpln1 24803 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
55 | 40 | ad5antr 745 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
56 | 1, 2, 32, 33, 8, 54, 55, 53 | perpcom 24806 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
57 | 1, 33, 32, 4, 13, 17, 9, 34 | ncolrot2 24656 |
. . . . . . . . . . . . . . . . . 18
         |
58 | | ioran 497 |
. . . . . . . . . . . . . . . . . 18
               |
59 | 57, 58 | sylib 201 |
. . . . . . . . . . . . . . . . 17
         |
60 | 59 | simpld 465 |
. . . . . . . . . . . . . . . 16
       |
61 | 60 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
             ⟂G       
      |
62 | | nelne2 2732 |
. . . . . . . . . . . . . . 15
     
       |
63 | 41, 61, 62 | syl2anc 671 |
. . . . . . . . . . . . . 14
             ⟂G          |
64 | 63 | ad4antr 743 |
. . . . . . . . . . . . 13
                 ⟂G        
       cgrG         
       ⟂G         hpG              |
65 | 64 | adantr 471 |
. . . . . . . . . . . 12
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
66 | 65 | necomd 2690 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
67 | 1, 32, 33, 8, 19, 45, 66 | tglinecom 24728 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                     |
68 | 56, 51, 67 | 3brtr3d 4445 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
69 | 1, 2, 32, 33, 8, 16, 12, 52, 19, 68 | perprag 24816 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                 ∟G    |
70 | 1, 2, 32, 4, 9, 13, 20, 24, 29, 38 | tgcgrneq 24575 |
. . . . . . . . . . . 12
   |
71 | 70 | necomd 2690 |
. . . . . . . . . . 11
   |
72 | 71 | ad7antr 749 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
73 | 70 | ad4antr 743 |
. . . . . . . . . . . . 13
               ⟂G       
        cgrG            |
74 | 73 | neneqd 2639 |
. . . . . . . . . . . 12
               ⟂G       
        cgrG         
  |
75 | 41 | orcd 398 |
. . . . . . . . . . . . . . . . . . . 20
             ⟂G                |
76 | 1, 33, 32, 5, 10, 14, 42, 75 | colrot2 24653 |
. . . . . . . . . . . . . . . . . . 19
             ⟂G                |
77 | 1, 33, 32, 5, 42, 10, 14, 76 | colcom 24651 |
. . . . . . . . . . . . . . . . . 18
             ⟂G                |
78 | 77 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
               ⟂G       
        cgrG                  |
79 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
               ⟂G       
        cgrG                 cgrG           |
80 | 1, 33, 32, 6, 11, 15, 43, 3, 22, 26, 46, 78, 79 | lnxfr 24659 |
. . . . . . . . . . . . . . . 16
               ⟂G       
        cgrG                  |
81 | 1, 33, 32, 6, 22, 46, 26, 80 | colrot2 24653 |
. . . . . . . . . . . . . . 15
               ⟂G       
        cgrG                  |
82 | 1, 33, 32, 6, 26, 22, 46, 81 | colcom 24651 |
. . . . . . . . . . . . . 14
               ⟂G       
        cgrG                  |
83 | 82 | orcomd 394 |
. . . . . . . . . . . . 13
               ⟂G       
        cgrG                  |
84 | 83 | ord 383 |
. . . . . . . . . . . 12
               ⟂G       
        cgrG          
       |
85 | 74, 84 | mpd 15 |
. . . . . . . . . . 11
               ⟂G       
        cgrG                |
86 | 85 | ad3antrrr 741 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
87 | 1, 32, 33, 8, 27, 23, 48, 72, 86 | lncom 24715 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
88 | | simprrr 780 |
. . . . . . . . . . . . 13
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
89 | 88 | eqcomd 2467 |
. . . . . . . . . . . 12
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
90 | 1, 2, 32, 8, 45, 19, 48, 28, 89, 65 | tgcgrneq 24575 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
91 | 1, 32, 33, 8, 48, 28, 90 | tgelrnln 24723 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
92 | 1, 32, 33, 8, 27, 23, 72 | tgelrnln 24723 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
93 | | simpllr 774 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
94 | | simplr 767 |
. . . . . . . . . . . . . . . 16
                 ⟂G        
       cgrG         
       ⟂G         hpG              |
95 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
                 ⟂G        
       cgrG         
       ⟂G         hpG                 ⟂G         |
96 | 33, 7, 95 | perpln2 24804 |
. . . . . . . . . . . . . . . 16
                 ⟂G        
       cgrG         
       ⟂G         hpG                  |
97 | 1, 32, 33, 7, 94, 47, 96 | tglnne 24721 |
. . . . . . . . . . . . . . 15
                 ⟂G        
       cgrG         
       ⟂G         hpG              |
98 | 97 | adantr 471 |
. . . . . . . . . . . . . 14
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
99 | 98 | necomd 2690 |
. . . . . . . . . . . . 13
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
100 | 1, 32, 33, 8, 48, 93, 99 | tgelrnln 24723 |
. . . . . . . . . . . 12
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
101 | 95 | adantr 471 |
. . . . . . . . . . . . 13
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
102 | 1, 32, 33, 8, 27, 23, 72 | tglinecom 24728 |
. . . . . . . . . . . . 13
       
          ⟂G                cgrG         

      ⟂G         hpG                                     |
103 | 1, 32, 33, 8, 48, 93, 100 | tglnne 24721 |
. . . . . . . . . . . . . 14
       
          ⟂G                cgrG         

      ⟂G         hpG                             |
104 | 1, 32, 33, 8, 48, 93, 103 | tglinecom 24728 |
. . . . . . . . . . . . 13
       
          ⟂G                cgrG         

      ⟂G         hpG                                     |
105 | 101, 102,
104 | 3brtr4d 4446 |
. . . . . . . . . . . 12
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
106 | 1, 2, 32, 33, 8, 92, 100, 105 | perpcom 24806 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
107 | | trgcopy.k |
. . . . . . . . . . . . . 14
hlG   |
108 | | simprrl 779 |
. . . . . . . . . . . . . 14
       
          ⟂G                cgrG         

      ⟂G         hpG                                   |
109 | 1, 32, 107, 28, 93, 48, 8, 33, 108 | hlln 24700 |
. . . . . . . . . . . . 13
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
110 | 1, 32, 33, 8, 48, 93, 28, 99, 109 | lncom 24715 |
. . . . . . . . . . . 12
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
111 | 110 | orcd 398 |
. . . . . . . . . . 11
       
          ⟂G                cgrG         

      ⟂G         hpG                                   |
112 | 1, 2, 32, 33, 8, 48, 93, 28, 106, 111, 90 | colperp 24819 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
113 | 1, 2, 32, 33, 8, 91, 92, 112 | perpcom 24806 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
114 | 1, 2, 32, 33, 8, 27, 23, 87, 28, 113 | perprag 24816 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                 ∟G    |
115 | 79 | ad3antrrr 741 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                                  cgrG           |
116 | 1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115 | cgr3simp2 24614 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
117 | 1, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 114, 116, 89 | hypcgr 24891 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
118 | | eqid 2461 |
. . . . . . . . 9
pInvG  pInvG   |
119 | 51, 68 | eqbrtrd 4436 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
120 | 1, 2, 32, 33, 8, 12, 16, 49, 19, 119 | perprag 24816 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                                 ∟G    |
121 | 1, 2, 32, 33, 118, 8, 12, 45, 19, 120 | ragcom 24791 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                 ∟G    |
122 | 102, 113 | eqbrtrrd 4438 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                ⟂G         |
123 | 1, 2, 32, 33, 8, 23, 27, 86, 28, 122 | perprag 24816 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                                 ∟G    |
124 | 1, 2, 32, 33, 118, 8, 23, 48, 28, 123 | ragcom 24791 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                 ∟G    |
125 | 1, 2, 32, 8, 45, 19, 48, 28, 89 | tgcgrcomlr 24572 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
126 | 1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 115 | cgr3simp3 24615 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
127 | 1, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 121, 124, 125, 126 | hypcgr 24891 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
128 | 1, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 117, 127 | trgcgr 24609 |
. . . . . 6
       
          ⟂G                cgrG         

      ⟂G         hpG                                  cgrG           |
129 | 1, 32, 33, 4, 20, 24, 70 | tgelrnln 24723 |
. . . . . . . . 9
       |
130 | 129 | ad4antr 743 |
. . . . . . . 8
               ⟂G       
        cgrG                |
131 | 130 | ad3antrrr 741 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                                 |
132 | | simpl 463 |
. . . . . . . . . . 11
 
   |
133 | | eqidd 2462 |
. . . . . . . . . . 11
 
               |
134 | 132, 133 | eleq12d 2533 |
. . . . . . . . . 10
 
                 |
135 | | simpr 467 |
. . . . . . . . . . 11
 
   |
136 | 135, 133 | eleq12d 2533 |
. . . . . . . . . 10
 
                 |
137 | 134, 136 | anbi12d 722 |
. . . . . . . . 9
 
                                 |
138 | | simpr 467 |
. . . . . . . . . . 11
       |
139 | | simpll 765 |
. . . . . . . . . . . 12
       |
140 | | simplr 767 |
. . . . . . . . . . . 12
       |
141 | 139, 140 | oveq12d 6332 |
. . . . . . . . . . 11
               |
142 | 138, 141 | eleq12d 2533 |
. . . . . . . . . 10
         
       |
143 | 142 | cbvrexdva 3037 |
. . . . . . . . 9
 
            
            |
144 | 137, 143 | anbi12d 722 |
. . . . . . . 8
 
                                                         |
145 | 144 | cbvopabv 4485 |
. . . . . . 7
                                                               |
146 | 8 | adantr 471 |
. . . . . . . . . . 11
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
    
TarskiG |
147 | 19 | adantr 471 |
. . . . . . . . . . 11
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
    
  |
148 | 16 | adantr 471 |
. . . . . . . . . . 11
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
    
  |
149 | 12 | adantr 471 |
. . . . . . . . . . 11
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
    
  |
150 | 23 | adantr 471 |
. . . . . . . . . . . . 13
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
    
  |
151 | 27 | adantr 471 |
. . . . . . . . . . . . 13
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
    
  |
152 | 28 | adantr 471 |
. . . . . . . . . . . . 13
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
       |
153 | 71 | ad8antr 751 |
. . . . . . . . . . . . . . . 16
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
       |
154 | | simpr 467 |
. . . . . . . . . . . . . . . 16
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
           |
155 | 1, 32, 33, 146, 151, 150, 152, 153, 154 | lncom 24715 |
. . . . . . . . . . . . . . 15
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
           |
156 | 155 | orcd 398 |
. . . . . . . . . . . . . 14
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
             |
157 | 1, 33, 32, 146, 151, 150, 152, 156 | colrot1 24652 |
. . . . . . . . . . . . 13
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
             |
158 | 128 | adantr 471 |
. . . . . . . . . . . . . 14
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
            cgrG           |
159 | 1, 2, 32, 3, 146, 149, 148, 147, 150, 151, 152, 158 | trgcgrcom 24621 |
. . . . . . . . . . . . 13
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
            cgrG           |
160 | 1, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159 | lnxfr 24659 |
. . . . . . . . . . . 12
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
             |
161 | 1, 33, 32, 146, 149, 147, 148, 160 | colrot1 24652 |
. . . . . . . . . . 11
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
             |
162 | 1, 33, 32, 146, 147, 148, 149, 161 | colcom 24651 |
. . . . . . . . . 10
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
             |
163 | 34 | ad8antr 751 |
. . . . . . . . . 10
                   ⟂G       
        cgrG          
      ⟂G         hpG                          
             |
164 | 162, 163 | pm2.65da 584 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                          
      |
165 | 108, 164 | jca 539 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                                         |
166 | 109 | orcd 398 |
. . . . . . . . . 10
       
          ⟂G                cgrG         

      ⟂G         hpG                                   |
167 | 1, 33, 32, 8, 93, 48, 28, 166 | colrot2 24653 |
. . . . . . . . 9
       
          ⟂G                cgrG         

      ⟂G         hpG                                   |
168 | 1, 32, 33, 8, 131, 28, 145, 93, 86, 167, 107 | colhp 24860 |
. . . . . . . 8
       
          ⟂G                cgrG         

      ⟂G         hpG                              hpG         
      
        |
169 | 165, 168 | mpbird 240 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                             hpG            |
170 | | trgcopy.f |
. . . . . . . . . 10
   |
171 | 170 | ad4antr 743 |
. . . . . . . . 9
               ⟂G       
        cgrG            |
172 | 171 | ad2antrr 737 |
. . . . . . . 8
                 ⟂G        
       cgrG         
       ⟂G         hpG              |
173 | 172 | adantr 471 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                          
  |
174 | | simplrr 776 |
. . . . . . 7
       
          ⟂G                cgrG         

      ⟂G         hpG                             hpG            |
175 | 1, 32, 33, 8, 131, 28, 145, 93, 169, 173, 174 | hpgtr 24858 |
. . . . . 6
       
          ⟂G                cgrG         

      ⟂G         hpG                             hpG            |
176 | 128, 175 | jca 539 |
. . . . 5
       
          ⟂G                cgrG         

      ⟂G         hpG                                   cgrG           hpG             |
177 | 1, 32, 107, 47, 44, 18, 7, 94, 2, 97, 64 | hlcgrex 24709 |
. . . . 5
                 ⟂G        
       cgrG         
       ⟂G         hpG            
       
      |
178 | 176, 177 | reximddv 2874 |
. . . 4
                 ⟂G        
       cgrG       |