for n being Nat
for L1, L2 being Element of line_of_REAL n
for P1, P2 being Element of plane_of_REAL n st L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 holds
P1 = P2