theorem Th5: :: EUCLMETR:5

for MS being OrtAfPl
for a, b, c being Element of MS st not LIN a,b,c holds
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )