theorem :: EUCLIDLP:94

for n being Nat
for x1, x2, x3 being Element of REAL n holds
( Line (x1,x2) c= plane (x1,x2,x3) & Line (x2,x3) c= plane (x1,x2,x3) & Line (x3,x1) c= plane (x1,x2,x3) )