theorem Th7: :: EUCLMETR:7

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