let POS be OrtAfPl; :: thesis: POS is OrtAfSp
for a, b, c, d, p, q, r, s being Element of POS st a,b _|_ p,q & a,b _|_ p,s holds
a,b _|_ q,s

proof

let a, b, c, d, p, q, r, s be Element of POS; :: thesis: ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s )
assume that
A1: a,b _|_ p,q and
A2: a,b _|_ p,s ; :: thesis: a,b _|_ q,s

A3: now :: thesis: ( a <> b & p <> q implies a,b _|_ q,s )

reconsider p9 = p, q9 = q, s9 = s as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
assume that
A4: a <> b and
A5: p <> q ; :: thesis: a,b _|_ q,s
p,q // p,s by A1, A2, A4, Def8;
then p9,q9 // p9,s9 by Th36;
then q9,p9 // q9,s9 by DIRAF:40;
then p9,q9 // q9,s9 by AFF_1:4;
then A6: p,q // q,s by Th36;
p,q _|_ a,b by A1, Def8;
hence a,b _|_ q,s by A5, A6, Def8; :: thesis: verum

end;

now :: thesis: ( a = b implies a,b _|_ q,s )

assume a = b ; :: thesis: a,b _|_ q,s
then q,s _|_ a,b by Def8;
hence a,b _|_ q,s by Def8; :: thesis: verum

end;

hence a,b _|_ q,s by A2, A3; :: thesis: verum

end;

then A7: for a, b, c, d, p, q, r, s being Element of POS holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) by Def8;
A8: for a, b, c being Element of POS st a <> b holds
ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c )

proof

let a, b, c be Element of POS; :: thesis: ( a <> b implies ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c ) )
assume A9: a <> b ; :: thesis: ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c )
consider y being Element of POS such that
A10: a,b _|_ c,y and
A11: c <> y by Def8;
reconsider a9 = a, b9 = b, c9 = c, y9 = y as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
not a9,b9 // c9,y9

proof

assume a9,b9 // c9,y9 ; :: thesis: contradiction
then a,b // c,y by Th36;
then c,y _|_ c,y by A9, A10, Def8;
hence contradiction by A11, Def8; :: thesis: verum

end;

then consider x9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A12: LIN a9,b9,x9 and
A13: LIN c9,y9,x9 by AFF_1:60;
reconsider x = x9 as Element of POS ;
c9,y9 // c9,x9 by A13, AFF_1:def 1;
then A14: c,y // c,x by Th36;
c,y _|_ a,b by A10, Def8;
then a,b _|_ c,x by A11, A14, Def8;
then A15: a,b _|_ x,c by Def8;
a9,b9 // a9,x9 by A12, AFF_1:def 1;
then a,b // a,x by Th36;
hence ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c ) by A15; :: thesis: verum

end;

( AffinStruct(# the carrier of POS, the CONGR of POS #) = AffinStruct(# the carrier of POS, the CONGR of POS #) & ( for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) ) ) by Def8;
hence POS is OrtAfSp by A8, A7, Def7; :: thesis: verum