theorem Th4: :: EUCLMETR:4

for MP being OrtAfSp
for x, y, z being Element of MP st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )