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

reconsider p' = p, q' = q, s' = s as Element of (Af POS) ;
assume that
A4: a <> b and
A5: p <> q ; :: thesis: a,b _|_ q,s
p,q // p,s by A1, A2, A4, Def10;
then p',q' // p',s' by Th48;
then q',p' // q',s' by DIRAF:47;
then p',q' // q',s' by AFF_1:13;
then A6: p,q // q,s by Th48;
p,q _|_ a,b by A1, Def10;
hence a,b _|_ q,s by A5, A6, Def10; :: thesis: verum

end;

now

assume a = b ; :: thesis: a,b _|_ q,s
then q,s _|_ a,b by Def10;
hence a,b _|_ q,s by Def10; :: 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 Def10;
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 Def10;
reconsider a' = a, b' = b, c' = c, y' = y as Element of (Af POS) ;
not a',b' // c',y'

proof

assume a',b' // c',y' ; :: thesis: contradiction
then a,b // c,y by Th48;
then c,y _|_ c,y by A9, A10, Def10;
hence contradiction by A11, Def10; :: thesis: verum

end;

then consider x' being Element of (Af POS) such that
A12: LIN a',b',x' and
A13: LIN c',y',x' by AFF_1:74;
reconsider x = x' as Element of POS ;
c',y' // c',x' by A13, AFF_1:def 1;
then A14: c,y // c,x by Th48;
c,y _|_ a,b by A10, Def10;
then a,b _|_ c,x by A11, A14, Def10;
then A15: a,b _|_ x,c by Def10;
a',b' // a',x' by A12, AFF_1:def 1;
then a,b // a,x by Th48;
hence ex x being Element of POS st
( a,b // a,x & a,b _|_ x,c ) by A15; :: thesis: verum

end;

( Af 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 Def10;
hence POS is OrtAfSp by A8, A7, Def9; :: thesis: verum