theorem Th90: :: EUCLIDLP:90

for n being Nat
for x1, x2, x3 being Element of REAL n holds plane (x1,x2,x3) in plane_of_REAL n ;