theorem :: DIRAF:18

for S being OAffinSpace
for a, b, c, d being Element of S holds
( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S )