theorem Th2: :: EUCLMETR:2

for MS being OrtAfPl
for a, b, c, d being Element of MS
for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )