theorem Th91: :: EUCLIDLP:91

for n being Nat
for x1, x2, x3 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P holds
plane (x1,x2,x3) c= P