:: deftheorem defines are_coplane EUCLIDLP:def 12 :
for n being Nat
for L1, L2 being Element of line_of_REAL n holds
( L1,L2 are_coplane iff ex x1, x2, x3 being Element of REAL n st
( L1 c= plane (x1,x2,x3) & L2 c= plane (x1,x2,x3) ) );