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 A 2

Proof

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