Step | Hyp | Ref
| Expression |
1 | | xp1st 6823 |
. . . . . . . . 9
         |
2 | 1 | ad2antrl 734 |
. . . . . . . 8
 
  

         |
3 | | xp1st 6823 |
. . . . . . . . 9
         |
4 | 3 | ad2antll 735 |
. . . . . . . 8
 
  

         |
5 | | simpl 459 |
. . . . . . . 8
 
  

     |
6 | | disjxpin.3 |
. . . . . . . . . . 11
 Disj
  |
7 | | disjors 4388 |
. . . . . . . . . . 11
Disj



 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
8 | 6, 7 | sylib 200 |
. . . . . . . . . 10
  
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
9 | | eqeq1 2455 |
. . . . . . . . . . . 12
    

       |
10 | | csbeq1 3366 |
. . . . . . . . . . . . . 14
    
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
11 | 10 | ineq1d 3633 |
. . . . . . . . . . . . 13
    
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
12 | 11 | eqeq1d 2453 |
. . . . . . . . . . . 12
    
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
13 | 9, 12 | orbi12d 716 |
. . . . . . . . . . 11
    
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
            ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
14 | | eqeq2 2462 |
. . . . . . . . . . . 12
    
                |
15 | | csbeq1 3366 |
. . . . . . . . . . . . . 14
    
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
16 | 15 | ineq2d 3634 |
. . . . . . . . . . . . 13
    
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
17 | 16 | eqeq1d 2453 |
. . . . . . . . . . . 12
    
        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
18 | 14, 17 | orbi12d 716 |
. . . . . . . . . . 11
    
             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
19 | 13, 18 | rspc2v 3159 |
. . . . . . . . . 10
                  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
20 | 8, 19 | syl5 33 |
. . . . . . . . 9
           
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
21 | 20 | imp 431 |
. . . . . . . 8
            
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
22 | 2, 4, 5, 21 | syl21anc 1267 |
. . . . . . 7
 
  

                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
23 | | xp2nd 6824 |
. . . . . . . . 9
         |
24 | 23 | ad2antrl 734 |
. . . . . . . 8
 
  

         |
25 | | xp2nd 6824 |
. . . . . . . . 9
         |
26 | 25 | ad2antll 735 |
. . . . . . . 8
 
  

         |
27 | | disjxpin.4 |
. . . . . . . . . . 11
 Disj
  |
28 | | disjors 4388 |
. . . . . . . . . . 11
Disj



 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
29 | 27, 28 | sylib 200 |
. . . . . . . . . 10
  
    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
30 | | eqeq1 2455 |
. . . . . . . . . . . 12
    

       |
31 | | csbeq1 3366 |
. . . . . . . . . . . . . 14
    
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
32 | 31 | ineq1d 3633 |
. . . . . . . . . . . . 13
    
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
33 | 32 | eqeq1d 2453 |
. . . . . . . . . . . 12
    
  
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif) 
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     |
34 | 30, 33 | orbi12d 716 |
. . . . . . . . . . 11
    
     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  
            ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      |
35 | | eqeq2 2462 |
. . . . . . . . . . . 12
    
                |
36 | | csbeq1 3366 |
. . . . . . . . . . . . . 14
    
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
37 | 36 | ineq2d 3634 |
. . . . . . . . . . . . 13
    
       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    |
38 | 37 | eqeq1d 2453 |
. . . . . . . . . . . 12
    
        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
39 | 35, 38 | orbi12d 716 |
. . . . . . . . . . 11
    
             ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
40 | 34, 39 | rspc2v 3159 |
. . . . . . . . . 10
                  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
41 | 29, 40 | syl5 33 |
. . . . . . . . 9
           
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
42 | 41 | imp 431 |
. . . . . . . 8
            
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
43 | 24, 26, 5, 42 | syl21anc 1267 |
. . . . . . 7
 
  

                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     |
44 | 22, 43 | jca 535 |
. . . . . 6
 
  

                    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      |
45 | | anddi 881 |
. . . . . 6
                  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   
                                    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)       |
46 | 44, 45 | sylib 200 |
. . . . 5
 
  

             
                 
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)       |
47 | | orass 527 |
. . . . 5
                                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    
                                    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        |
48 | 46, 47 | sylib 200 |
. . . 4
 
  

                                       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        |
49 | | xpopth 6832 |
. . . . . . 7
   
                     
   |
50 | 49 | adantl 468 |
. . . . . 6
 
  

                     
   |
51 | 50 | biimpd 211 |
. . . . 5
 
  

                         |
52 | | inss2 3653 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
53 | | csbin 3799 |
. . . . . . . . . . . 12
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
54 | | csbin 3799 |
. . . . . . . . . . . 12
  ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
55 | 53, 54 | ineq12i 3632 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
56 | | in4 3648 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)    |
57 | 55, 56 | eqtri 2473 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
58 | | vex 3048 |
. . . . . . . . . . . . 13
 |
59 | | csbnestg 3787 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . 12
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
61 | | fvex 5875 |
. . . . . . . . . . . . . 14
     |
62 | | disjxpin.2 |
. . . . . . . . . . . . . 14
    
  |
63 | 61, 62 | csbie 3389 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)  |
64 | 63 | csbeq2i 3782 |
. . . . . . . . . . . 12
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
65 | | csbfv 5902 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)          |
66 | | csbeq1 3366 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)        
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)   |
67 | 65, 66 | ax-mp 5 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)  |
68 | 60, 64, 67 | 3eqtr3ri 2482 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
69 | | vex 3048 |
. . . . . . . . . . . . 13
 |
70 | | csbnestg 3787 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . 12
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
72 | 63 | csbeq2i 3782 |
. . . . . . . . . . . 12
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
73 | | csbfv 5902 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)          |
74 | | csbeq1 3366 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)        
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)   |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . . 12
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)  |
76 | 71, 72, 75 | 3eqtr3ri 2482 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
77 | 68, 76 | ineq12i 3632 |
. . . . . . . . . 10
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
78 | 52, 57, 77 | 3sstr4i 3471 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
79 | | sseq0 3766 |
. . . . . . . . 9
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)      |
80 | 78, 79 | mpan 676 |
. . . . . . . 8
        ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)      |
81 | 80 | a1i 11 |
. . . . . . 7
 
  

           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)       |
82 | 81 | adantld 469 |
. . . . . 6
 
  

                    ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
   ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)       |
83 | | inss1 3652 |
. . . . . . . . . . 11
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
84 | | csbnestg 3787 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
85 | 58, 84 | ax-mp 5 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
86 | | fvex 5875 |
. . . . . . . . . . . . . . 15
     |
87 | | disjxpin.1 |
. . . . . . . . . . . . . . 15
    
  |
88 | 86, 87 | csbie 3389 |
. . . . . . . . . . . . . 14
      ![]_ ]_](_urbrack.gif)  |
89 | 88 | csbeq2i 3782 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
90 | | csbfv 5902 |
. . . . . . . . . . . . . 14
  ![]_ ]_](_urbrack.gif)          |
91 | | csbeq1 3366 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)        
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)   |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)  |
93 | 85, 89, 92 | 3eqtr3ri 2482 |
. . . . . . . . . . . 12
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
94 | | csbnestg 3787 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   |
95 | 69, 94 | ax-mp 5 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
96 | 88 | csbeq2i 3782 |
. . . . . . . . . . . . 13
  ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
97 | | csbfv 5902 |
. . . . . . . . . . . . . 14
  ![]_ ]_](_urbrack.gif)          |
98 | | csbeq1 3366 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)        
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)   |
99 | 97, 98 | ax-mp 5 |
. . . . . . . . . . . . 13
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)  |
100 | 95, 96, 99 | 3eqtr3ri 2482 |
. . . . . . . . . . . 12
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
101 | 93, 100 | ineq12i 3632 |
. . . . . . . . . . 11
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
102 | 83, 57, 101 | 3sstr4i 3471 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
103 | | sseq0 3766 |
. . . . . . . . . 10
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)      |
104 | 102, 103 | mpan 676 |
. . . . . . . . 9
        ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)      |
105 | 104 | a1i 11 |
. . . . . . . 8
 
  

           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)       |
106 | 105 | adantrd 470 |
. . . . . . 7
 
  

            ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)       |
107 | 81 | adantld 469 |
. . . . . . 7
 
  

            ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)  
   ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)       |
108 | 106, 107 | jaod 382 |
. . . . . 6
 
  

             ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     
 ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)       |
109 | 82, 108 | jaod 382 |
. . . . 5
 
  

             
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)  
  ![]_ ]_](_urbrack.gif)       |
110 | 51, 109 | orim12d 849 |
. . . 4
 
  

             
                          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)  
         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)        |
111 | 48, 110 | mpd 15 |
. . 3
 
  

       ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)       |
112 | 111 | ralrimivva 2809 |
. 2
             ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)       |
113 | | disjors 4388 |
. 2
Disj                  ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)       |
114 | 112, 113 | sylibr 216 |
1
 Disj
       |