let POS be OrtAfSp; :: thesis: ( Af POS is AffinPlane implies POS is OrtAfPl )
assume A1: Af POS is AffinPlane ; :: thesis: POS is OrtAfPl

A2: now

let a, b, c, d, p, q, r, s be Element of ; :: thesis: ( ( 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 _|_ r,s & not p,q // r,s implies a = b ) )
thus ( ( 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 ) ) by Def9; :: thesis: ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b )
thus ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) :: thesis: verum

proof

reconsider a' = a, b' = b, p' = p, q' = q, r' = r, s' = s as Element of ;
assume that
A3: a,b _|_ p,q and
A4: a,b _|_ r,s ; :: thesis: ( p,q // r,s or a = b )
A5: p,q _|_ a,b by A3, Def9;
A6: r,s _|_ a,b by A4, Def9;
assume A7: ( not p,q // r,s & not a = b ) ; :: thesis: contradiction
then A8: not p',q' // r',s' by Th48;
then A9: p' <> q' by AFF_1:12;
consider x' being Element of such that
A10: LIN p',q',x' and
A11: LIN r',s',x' by A1, A8, AFF_1:74;
reconsider x = x' as Element of ;
A12: r' <> s' by A8, AFF_1:12;
LIN s',r',x' by A11, AFF_1:15;
then s',r' // s',x' by AFF_1:def 1;
then A13: r',s' // x',s' by AFF_1:13;
then r,s // x,s by Th48;
then a,b _|_ x,s by A12, A6, Def9;
then A14: x,s _|_ a,b by Def9;
LIN q',p',x' by A10, AFF_1:15;
then q',p' // q',x' by AFF_1:def 1;
then p',q' // x',q' by AFF_1:13;
then p,q // x,q by Th48;
then A15: a,b _|_ x,q by A9, A5, Def9;

A16: now

consider y' being Element of such that
A17: ( a',b' // q',y' & q' <> y' ) by DIRAF:47;
assume that
A18: x <> q and
A19: x <> s ; :: thesis: contradiction
not q',y' // x',s'

proof

assume q',y' // x',s' ; :: thesis: contradiction
then q',y' // r',s' by A13, A19, AFF_1:14;
then r',s' // a',b' by A17, AFF_1:14;
then r,s // a,b by Th48;
then a,b _|_ a,b by A12, A6, Def9;
hence contradiction by A7, Def9; :: thesis: verum

end;

then consider z' being Element of such that
A20: LIN q',y',z' and
A21: LIN x',s',z' by A1, AFF_1:74;
reconsider z = z' as Element of ;
q',y' // q',z' by A20, AFF_1:def 1;
then a',b' // q',z' by A17, AFF_1:14;
then A22: a,b // q,z by Th48;
A23: x',s' // x',z' by A21, AFF_1:def 1;
then x,s // x,z by Th48;
then a,b _|_ x,z by A14, A19, Def9;
then a,b _|_ q,z by A15, Def9;
then q,z _|_ q,z by A7, A22, Def9;
then x',s' // x',q' by A23, Def9;
then A24: LIN x',s',q' by AFF_1:def 1;
( LIN x',s',x' & LIN x',q',p' ) by A10, AFF_1:15, AFF_1:16;
then LIN x',s',p' by A18, A24, AFF_1:20;
then x',s' // p',q' by A24, AFF_1:19;
then p',q' // r',s' by A13, A19, AFF_1:14;
hence contradiction by A7, Th48; :: thesis: verum

end;

r',s' // r',x' by A11, AFF_1:def 1;
then A25: r',s' // x',r' by AFF_1:13;
then r,s // x,r by Th48;
then a,b _|_ x,r by A12, A6, Def9;
then A26: x,r _|_ a,b by Def9;

A27: now

consider y' being Element of such that
A28: ( a',b' // q',y' & q' <> y' ) by DIRAF:47;
assume that
A29: x <> q and
A30: x <> r ; :: thesis: contradiction
not q',y' // x',r'

proof

assume q',y' // x',r' ; :: thesis: contradiction
then q',y' // r',s' by A25, A30, AFF_1:14;
then r',s' // a',b' by A28, AFF_1:14;
then r,s // a,b by Th48;
then a,b _|_ a,b by A12, A6, Def9;
hence contradiction by A7, Def9; :: thesis: verum

end;

then consider z' being Element of such that
A31: LIN q',y',z' and
A32: LIN x',r',z' by A1, AFF_1:74;
reconsider z = z' as Element of ;
q',y' // q',z' by A31, AFF_1:def 1;
then a',b' // q',z' by A28, AFF_1:14;
then A33: a,b // q,z by Th48;
A34: x',r' // x',z' by A32, AFF_1:def 1;
then x,r // x,z by Th48;
then a,b _|_ x,z by A26, A30, Def9;
then a,b _|_ q,z by A15, Def9;
then q,z _|_ q,z by A7, A33, Def9;
then x',r' // x',q' by A34, Def9;
then A35: LIN x',r',q' by AFF_1:def 1;
( LIN x',r',x' & LIN x',q',p' ) by A10, AFF_1:15, AFF_1:16;
then LIN x',r',p' by A29, A35, AFF_1:20;
then x',r' // p',q' by A35, AFF_1:19;
then p',q' // r',s' by A25, A30, AFF_1:14;
hence contradiction by A7, Th48; :: thesis: verum

end;

p',q' // p',x' by A10, AFF_1:def 1;
then p',q' // x',p' by AFF_1:13;
then p,q // x,p by Th48;
then A36: a,b _|_ x,p by A9, A5, Def9;

A37: now

consider y' being Element of such that
A38: ( a',b' // p',y' & p' <> y' ) by DIRAF:47;
assume that
A39: x <> p and
A40: x <> s ; :: thesis: contradiction
not p',y' // x',s'

proof

assume p',y' // x',s' ; :: thesis: contradiction
then p',y' // r',s' by A13, A40, AFF_1:14;
then r',s' // a',b' by A38, AFF_1:14;
then r,s // a,b by Th48;
then a,b _|_ a,b by A12, A6, Def9;
hence contradiction by A7, Def9; :: thesis: verum

end;

then consider z' being Element of such that
A41: LIN p',y',z' and
A42: LIN x',s',z' by A1, AFF_1:74;
reconsider z = z' as Element of ;
p',y' // p',z' by A41, AFF_1:def 1;
then a',b' // p',z' by A38, AFF_1:14;
then A43: a,b // p,z by Th48;
A44: x',s' // x',z' by A42, AFF_1:def 1;
then x,s // x,z by Th48;
then a,b _|_ x,z by A14, A40, Def9;
then a,b _|_ p,z by A36, Def9;
then p,z _|_ p,z by A7, A43, Def9;
then x',s' // x',p' by A44, Def9;
then A45: LIN x',s',p' by AFF_1:def 1;
( LIN x',s',x' & LIN x',p',q' ) by A10, AFF_1:15, AFF_1:16;
then LIN x',s',q' by A39, A45, AFF_1:20;
then x',s' // p',q' by A45, AFF_1:19;
then p',q' // r',s' by A13, A40, AFF_1:14;
hence contradiction by A7, Th48; :: thesis: verum

end;

now

consider y' being Element of such that
A46: ( a',b' // p',y' & p' <> y' ) by DIRAF:47;
assume that
A47: x <> p and
A48: x <> r ; :: thesis: contradiction
not p',y' // x',r'

proof

assume p',y' // x',r' ; :: thesis: contradiction
then p',y' // r',s' by A25, A48, AFF_1:14;
then r',s' // a',b' by A46, AFF_1:14;
then r,s // a,b by Th48;
then a,b _|_ a,b by A12, A6, Def9;
hence contradiction by A7, Def9; :: thesis: verum

end;

then consider z' being Element of such that
A49: LIN p',y',z' and
A50: LIN x',r',z' by A1, AFF_1:74;
reconsider z = z' as Element of ;
p',y' // p',z' by A49, AFF_1:def 1;
then a',b' // p',z' by A46, AFF_1:14;
then A51: a,b // p,z by Th48;
A52: x',r' // x',z' by A50, AFF_1:def 1;
then x,r // x,z by Th48;
then a,b _|_ x,z by A26, A48, Def9;
then a,b _|_ p,z by A36, Def9;
then p,z _|_ p,z by A7, A51, Def9;
then x',r' // x',p' by A52, Def9;
then A53: LIN x',r',p' by AFF_1:def 1;
( LIN x',r',x' & LIN x',p',q' ) by A10, AFF_1:15, AFF_1:16;
then LIN x',r',q' by A47, A53, AFF_1:20;
then x',r' // p',q' by A53, AFF_1:19;
then p',q' // r',s' by A25, A48, AFF_1:14;
hence contradiction by A7, Th48; :: thesis: verum

end;

hence contradiction by A8, A37, A27, A16, AFF_1:12; :: thesis: verum

end;

end;

for a, b, c being Element of ex x being Element of st
( a,b _|_ c,x & c <> x ) by Def9;
hence POS is OrtAfPl by A1, A2, Def10; :: thesis: verum