theorem :: ANALMETR:64

for POS being OrtAfPl
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds
M // N