let POS be OrtAfSp; :: thesis: ( Af POS is AffinPlane implies POS is OrtAfPl )
assume A1: Af POS is AffinPlane ; :: thesis: POS is OrtAfPl
A2: for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) by Def9;

now

let a, b, c, d, p, q, r, s be Element of POS; :: 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

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

A12: now

assume A13: ( x <> p & x <> r ) ; :: thesis: contradiction
consider y' being Element of (Af POS) such that
A14: ( a',b' // p',y' & p' <> y' ) by DIRAF:47;
not p',y' // x',r'

proof

assume p',y' // x',r' ; :: thesis: contradiction
then p',y' // r',s' by A9, A13, AFF_1:14;
then r',s' // a',b' by A14, AFF_1:14;
then r,s // a,b by Th48;
then a,b _|_ a,b by A6, A8, Def9;
hence contradiction by A4, Def9; :: thesis: verum

end;

then consider z' being Element of (Af POS) such that
A15: ( LIN p',y',z' & LIN x',r',z' ) by A1, AFF_1:74;
reconsider z = z' as Element of the carrier of POS ;
A16: ( p',y' // p',z' & x',r' // x',z' ) by A15, AFF_1:def 1;
then a',b' // p',z' by A14, AFF_1:14;
then A17: a,b // p,z by Th48;
x,r // x,z by A16, Th48;
then a,b _|_ x,z by A11, A13, Def9;
then a,b _|_ p,z by A10, Def9;
then p,z _|_ p,z by A4, A17, Def9;
then x',r' // x',p' by A16, Def9;
then A18: LIN x',r',p' by AFF_1:def 1;
( LIN x',r',x' & LIN x',p',q' ) by A7, AFF_1:15, AFF_1:16;
then LIN x',r',q' by A13, A18, AFF_1:20;
then x',r' // p',q' by A18, AFF_1:19;
then p',q' // r',s' by A9, A13, AFF_1:14;
hence contradiction by A4, Th48; :: thesis: verum

end;

A19: now

assume A20: ( x <> p & x <> s ) ; :: thesis: contradiction
consider y' being Element of (Af POS) such that
A21: ( a',b' // p',y' & p' <> y' ) by DIRAF:47;
not p',y' // x',s'

proof

assume p',y' // x',s' ; :: thesis: contradiction
then p',y' // r',s' by A9, A20, AFF_1:14;
then r',s' // a',b' by A21, AFF_1:14;
then r,s // a,b by Th48;
then a,b _|_ a,b by A6, A8, Def9;
hence contradiction by A4, Def9; :: thesis: verum

end;

then consider z' being Element of (Af POS) such that
A22: ( LIN p',y',z' & LIN x',s',z' ) by A1, AFF_1:74;
reconsider z = z' as Element of the carrier of POS ;
A23: ( p',y' // p',z' & x',s' // x',z' ) by A22, AFF_1:def 1;
then a',b' // p',z' by A21, AFF_1:14;
then A24: a,b // p,z by Th48;
x,s // x,z by A23, Th48;
then a,b _|_ x,z by A11, A20, Def9;
then a,b _|_ p,z by A10, Def9;
then p,z _|_ p,z by A4, A24, Def9;
then x',s' // x',p' by A23, Def9;
then A25: LIN x',s',p' by AFF_1:def 1;
( LIN x',s',x' & LIN x',p',q' ) by A7, AFF_1:15, AFF_1:16;
then LIN x',s',q' by A20, A25, AFF_1:20;
then x',s' // p',q' by A25, AFF_1:19;
then p',q' // r',s' by A9, A20, AFF_1:14;
hence contradiction by A4, Th48; :: thesis: verum

end;

A26: now

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

proof

assume q',y' // x',r' ; :: thesis: contradiction
then q',y' // r',s' by A9, A27, 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 A6, A8, Def9;
hence contradiction by A4, Def9; :: thesis: verum

end;

then consider z' being Element of (Af POS) such that
A29: ( LIN q',y',z' & LIN x',r',z' ) by A1, AFF_1:74;
reconsider z = z' as Element of the carrier of POS ;
A30: ( q',y' // q',z' & x',r' // x',z' ) by A29, AFF_1:def 1;
then a',b' // q',z' by A28, AFF_1:14;
then A31: a,b // q,z by Th48;
x,r // x,z by A30, Th48;
then a,b _|_ x,z by A11, A27, Def9;
then a,b _|_ q,z by A10, Def9;
then q,z _|_ q,z by A4, A31, Def9;
then x',r' // x',q' by A30, Def9;
then A32: LIN x',r',q' by AFF_1:def 1;
( LIN x',r',x' & LIN x',q',p' ) by A7, AFF_1:15, AFF_1:16;
then LIN x',r',p' by A27, A32, AFF_1:20;
then x',r' // p',q' by A32, AFF_1:19;
then p',q' // r',s' by A9, A27, AFF_1:14;
hence contradiction by A4, Th48; :: thesis: verum

end;

now

assume A33: ( x <> q & x <> s ) ; :: thesis: contradiction
consider y' being Element of (Af POS) such that
A34: ( a',b' // q',y' & q' <> y' ) by DIRAF:47;
not q',y' // x',s'

proof

assume q',y' // x',s' ; :: thesis: contradiction
then q',y' // r',s' by A9, A33, AFF_1:14;
then r',s' // a',b' by A34, AFF_1:14;
then r,s // a,b by Th48;
then a,b _|_ a,b by A6, A8, Def9;
hence contradiction by A4, Def9; :: thesis: verum

end;

then consider z' being Element of (Af POS) such that
A35: ( LIN q',y',z' & LIN x',s',z' ) by A1, AFF_1:74;
reconsider z = z' as Element of the carrier of POS ;
A36: ( q',y' // q',z' & x',s' // x',z' ) by A35, AFF_1:def 1;
then a',b' // q',z' by A34, AFF_1:14;
then A37: a,b // q,z by Th48;
x,s // x,z by A36, Th48;
then a,b _|_ x,z by A11, A33, Def9;
then a,b _|_ q,z by A10, Def9;
then q,z _|_ q,z by A4, A37, Def9;
then x',s' // x',q' by A36, Def9;
then A38: LIN x',s',q' by AFF_1:def 1;
( LIN x',s',x' & LIN x',q',p' ) by A7, AFF_1:15, AFF_1:16;
then LIN x',s',p' by A33, A38, AFF_1:20;
then x',s' // p',q' by A38, AFF_1:19;
then p',q' // r',s' by A9, A33, AFF_1:14;
hence contradiction by A4, Th48; :: thesis: verum

end;

hence contradiction by A5, A12, A19, A26, AFF_1:12; :: thesis: verum

end;

end;

hence POS is OrtAfPl by A1, A2, Def10; :: thesis: verum