theorem Th12: :: EUCLID12:15

for OO, Ox, Oy being Element of REAL 2 st OO = |[0,0]| & Ox = |[1,0]| & Oy = |[0,1]| holds
REAL 2 = plane (OO,Ox,Oy)