reconsider OO = |[0,0]|, Ox = |[1,0]|, Oy = |[0,1]| as Element of REAL 2 by EUCLID:22;
REAL 2 = plane (OO,Ox,Oy) by Th12;
then REAL 2 in { P where P is Subset of (REAL 2) : ex x1, x2, x3 being Element of REAL 2 st P = plane (x1,x2,x3) } ;
hence REAL 2 is Element of plane_of_REAL 2 by EUCLIDLP:def 11; :: thesis: verum