Metamath Proof Explorer


Theorem resqcli

Description: Closure of square in reals. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypothesis resqcl.1 A
Assertion resqcli A2

Proof

Step Hyp Ref Expression
1 resqcl.1 A
2 resqcl AA2
3 1 2 ax-mp A2