theorem Th37: :: ANALMETR:37

for POS being OrtAfPl holds POS is OrtAfSp