theorem Th83: :: EUCLIDLP:83

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