theorem Th13: :: EUCLID12:16

REAL 2 is Element of plane_of_REAL 2