let POS be OrtAfPl; :: thesis: POS is OrtAfSp
A1: Af POS = AffinStruct(# the carrier of POS,the CONGR of POS #) ;
A2: for a, b, c being Element of POS ex x being Element of the carrier of POS st
( a,b _|_ c,x & c <> x ) by Def10;
A3: 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 A4: ( a,b _|_ p,q & a,b _|_ p,s ) ; :: thesis: a,b _|_ q,s

A5: 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;

now

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

end;

hence a,b _|_ q,s by A4, A5; :: thesis: verum

end;

A9: 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 A10: 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
A11: ( a,b _|_ c,y & 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 A10, A11, Def10;
hence contradiction by A11, Def10; :: thesis: verum

end;

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

end;

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 A3, Def10;
hence POS is OrtAfSp by A1, A2, A9, Def9; :: thesis: verum