<<< native
[ ESymbol Op "\8704"
, EIdentifier "A"
, ESpace (1 % 6)
, ESymbol Op "\8707"
, EIdentifier "P"
, ESpace (1 % 6)
, ESymbol Op "\8704"
, EIdentifier "B"
, ESpace (1 % 6)
, EDelimited
    "["
    "]"
    [ Right (EIdentifier "B")
    , Right (ESymbol Rel "\8712")
    , Right (EIdentifier "P")
    , Right (ESymbol Rel "\8660")
    , Right (ESymbol Op "\8704")
    , Right (EIdentifier "C")
    , Right (ESpace (1 % 6))
    , Right
        (EDelimited
           "("
           ")"
           [ Right (EIdentifier "C")
           , Right (ESymbol Rel "\8712")
           , Right (EIdentifier "B")
           , Right (ESymbol Rel "\8658")
           , Right (EIdentifier "C")
           , Right (ESymbol Rel "\8712")
           , Right (EIdentifier "A")
           ])
    ]
]
>>> omml
<?xml version='1.0' ?>
<m:oMathPara>
  <m:oMathParaPr>
    <m:jc m:val="center" />
  </m:oMathParaPr>
  <m:oMath>
    <m:r>
      <m:rPr>
        <m:sty m:val="p" />
      </m:rPr>
      <m:t>∀</m:t>
    </m:r>
    <m:r>
      <m:t>A</m:t>
    </m:r>
    <m:r>
      <m:t> </m:t>
    </m:r>
    <m:r>
      <m:rPr>
        <m:sty m:val="p" />
      </m:rPr>
      <m:t>∃</m:t>
    </m:r>
    <m:r>
      <m:t>P</m:t>
    </m:r>
    <m:r>
      <m:t> </m:t>
    </m:r>
    <m:r>
      <m:rPr>
        <m:sty m:val="p" />
      </m:rPr>
      <m:t>∀</m:t>
    </m:r>
    <m:r>
      <m:t>B</m:t>
    </m:r>
    <m:r>
      <m:t> </m:t>
    </m:r>
    <m:d>
      <m:dPr>
        <m:begChr m:val="[" />
        <m:endChr m:val="]" />
        <m:sepChr m:val="" />
        <m:grow />
      </m:dPr>
      <m:e>
        <m:r>
          <m:t>B</m:t>
        </m:r>
        <m:r>
          <m:rPr>
            <m:sty m:val="p" />
          </m:rPr>
          <m:t>∈</m:t>
        </m:r>
        <m:r>
          <m:t>P</m:t>
        </m:r>
        <m:r>
          <m:rPr>
            <m:sty m:val="p" />
          </m:rPr>
          <m:t>⇔</m:t>
        </m:r>
        <m:r>
          <m:rPr>
            <m:sty m:val="p" />
          </m:rPr>
          <m:t>∀</m:t>
        </m:r>
        <m:r>
          <m:t>C</m:t>
        </m:r>
        <m:r>
          <m:t> </m:t>
        </m:r>
        <m:d>
          <m:dPr>
            <m:begChr m:val="(" />
            <m:endChr m:val=")" />
            <m:sepChr m:val="" />
            <m:grow />
          </m:dPr>
          <m:e>
            <m:r>
              <m:t>C</m:t>
            </m:r>
            <m:r>
              <m:rPr>
                <m:sty m:val="p" />
              </m:rPr>
              <m:t>∈</m:t>
            </m:r>
            <m:r>
              <m:t>B</m:t>
            </m:r>
            <m:r>
              <m:rPr>
                <m:sty m:val="p" />
              </m:rPr>
              <m:t>⇒</m:t>
            </m:r>
            <m:r>
              <m:t>C</m:t>
            </m:r>
            <m:r>
              <m:rPr>
                <m:sty m:val="p" />
              </m:rPr>
              <m:t>∈</m:t>
            </m:r>
            <m:r>
              <m:t>A</m:t>
            </m:r>
          </m:e>
        </m:d>
      </m:e>
    </m:d>
  </m:oMath>
</m:oMathPara>