P0 & P11
      & P398 & P80
      & 
     (a0 = "3.2.vi" & a0 = "negeqsymm" & 
     a0 = "negeqsymm"
      & a0 = "lemma 1.1" & a0 = "rinv" & 
     a0 = "mid"
      & a0 = "mcom" & a0 = "thm 3.1.ii" & 
     a0 = "negeqsymm"
      & a0 = "minv" & a0 = "symm" & 
     a0 = "mas" & a0 = "mcom"
      & a0 = "mcom" & a0 = "mcom" & 
     a0 = "ordmult"
      & a0 = "thm 3.2.iv" & a0 = "symm" & 
     a0 = "negeqsymm"
      & a0 = "minv" & a0 = "thm 3.2.v"
      & P0) & 
     ((P11 & P74) & 
     (P10 & P73)
      & (P9 & P52) & 
     (P8 & P44)
      & (P7 & P41) & 
     (P6 & P41)
      & (P5 & P39) & 
     (P4 & P27)
      & (P3 & P16) & 
     (P2 & P15) & P0) & P0
\