theorem :: ARYTM1_5
x <= y & y <= x implies x = y ;

----------------------

<kxml>
<text source = ARYTM1_5>
<sentence>
<relation>
<builtInRelation>
Implication
<argument>
<logicalOperator>
&& /* Логическое И (&) */
</logicalOperator>
<sentence>
<sentence>
<mathRelation>
<=
</mathRelation>
<formula>
<variable>
x
</variable>
</formula>
<formula>
<variable>
y
</variable>
</formula>
</sentence>
</sentence>
<sentence>
<sentence>
<mathRelation>
<=
</mathRelation>
<formula>
<variable>
y
</variable>
</formula>
<formula>
<variable>
x
</variable>
</formula>
</sentence>
</sentence>
</argument>
<argument>
<sentence>
<mathRelation>
==
</mathRelation>
<formula>
<variable>
x
</variable>
</formula>
<formula>
<variable>
y
</variable>
</formula>
</sentence>
</argument>
</builtInRelation>
</relation>
</sentence>
</text>
</kxml>



It is right