theorem Th58: :: ANALMETR:58

for POS being OrtAfSp
for a, b, c being Element of POS holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )