:: deftheorem defines // ANALMETR:def 15 :
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K // M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line (a,b) & M = Line (c,d) & a,b // c,d ) );