theorem Th54: :: EUCLID_3:54

for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
plane (p1,p2,p3) = REAL 2