(
     (a0 = "Half" & Half = Inv(Two)) & (a0 = "Two" & Two = One
      + One) & 
     (a0 = "Three" & Three = One + 
     One + One)
      & (a0 = "Projtwo"
      & Projtwo(x1) = {x2|
     (Ex3.x2 E x3 & x3 E x1) & (Ax3.(Ax4.
     x2 E x3 & x2 E x4 & x3 E x1
      & x4 E x1 -> x3 = x4))}) & (
     a0 = "Si"
      & Si(x1) = {x2|(Ax3.x3 E x1 -> x2 E x3)}) & 
     (
     a0 = "Kpair" & x1 Kpair x2 = Sing(x1)
      Couple x1 Couple x2) & 
     (a0 = "Couple" & x1
      Couple x2 = {x3|x3 = x1 v x3 = x2})
      & (
     a0 = "Sing" & Sing(x1) = {x2|x2 = x1}) & (
     a0 = "Union"
      & x1 Union x2 = {x3|x3 E x1 v x3 E x2}) & (
     a0 = "Closure"
      & x1 Closure x2 = {x3|(Ax4.x1 E x4
      & (Ax5.p1(x5) E x4
      & x5 E x2 -> p2(x5) E x4)
      -> x3 E x4)}) & (a0 = "Reals"
      & Reals = {x1|Real(x1)}) & (
     a0 = "Nat"
      & Nat = {x1|(Ax2.
     Zero E x2 & (Ax3.x3 E x2
      -> x3 + One E x2) -> x1 E x2)})
      & P0) & (
     (
     a0 = "Sequence" & (Sequence(x1)
      == x1 Function [Nat,Reals]))
      & (a0 = "Function"
      & (
     x1 Function x2 == 
     (Ax3.x3 E x1 -> p1(x3) E p1(x2)
      & p2(x3) E p2(x2)) & (Ax3.(Ax4.(Ax5.[x3,x5] E x1
      & [x4,x5] E x1
      -> x3 = x4)))))
      & 
     (a0 = "<=" & (
     x1 <= x2
      == x1 Equal x2 v x1 < x2)) & 
     (a0 = "Equal" & (
     x1 Equal x2
      == x1 + Zero = x2 + Zero)) & P0)
      & P0
\