theorem Th82: :: EUCLIDLP:82
for n being Nat
for x1, x2, x3 being Element of REAL n holds
( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) )