theorem Th52: :: ANALMETR:52
for POS being OrtAfSp
for K, M, N being Subset of POS st K _|_ M & K // N holds
N _|_ M