let POS be OrtAfSp; :: thesis: ( AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane implies POS is OrtAfPl )
assume A1: AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane ; :: thesis: POS is OrtAfPl

A2: now :: thesis: 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 _|_ r,s & not p,q // r,s implies a = b ) )

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 Def7; :: 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 a9 = a, b9 = b, p9 = p, q9 = q, r9 = r, s9 = s as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
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, Def7;
A6: r,s _|_ a,b by A4, Def7;
assume A7: ( not p,q // r,s & not a = b ) ; :: thesis: contradiction
then A8: not p9,q9 // r9,s9 by Th36;
then A9: p9 <> q9 by AFF_1:3;
consider x9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A10: LIN p9,q9,x9 and
A11: LIN r9,s9,x9 by A1, A8, AFF_1:60;
reconsider x = x9 as Element of POS ;
A12: r9 <> s9 by A8, AFF_1:3;
LIN s9,r9,x9 by A11, AFF_1:6;
then s9,r9 // s9,x9 by AFF_1:def 1;
then A13: r9,s9 // x9,s9 by AFF_1:4;
then r,s // x,s by Th36;
then a,b _|_ x,s by A12, A6, Def7;
then A14: x,s _|_ a,b by Def7;
LIN q9,p9,x9 by A10, AFF_1:6;
then q9,p9 // q9,x9 by AFF_1:def 1;
then p9,q9 // x9,q9 by AFF_1:4;
then p,q // x,q by Th36;
then A15: a,b _|_ x,q by A9, A5, Def7;

A16: now :: thesis: ( x <> q implies not x <> s )

consider y9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A17: ( a9,b9 // q9,y9 & q9 <> y9 ) by DIRAF:40;
assume that
A18: x <> q and
A19: x <> s ; :: thesis: contradiction
not q9,y9 // x9,s9

proof

assume q9,y9 // x9,s9 ; :: thesis: contradiction
then q9,y9 // r9,s9 by A13, A19, AFF_1:5;
then r9,s9 // a9,b9 by A17, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def7;
hence contradiction by A7, Def7; :: thesis: verum

end;

then consider z9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A20: LIN q9,y9,z9 and
A21: LIN x9,s9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
q9,y9 // q9,z9 by A20, AFF_1:def 1;
then a9,b9 // q9,z9 by A17, AFF_1:5;
then A22: a,b // q,z by Th36;
A23: x9,s9 // x9,z9 by A21, AFF_1:def 1;
then x,s // x,z by Th36;
then a,b _|_ x,z by A14, A19, Def7;
then a,b _|_ q,z by A15, Def7;
then q,z _|_ q,z by A7, A22, Def7;
then x9,s9 // x9,q9 by A23, Def7;
then A24: LIN x9,s9,q9 by AFF_1:def 1;
( LIN x9,s9,x9 & LIN x9,q9,p9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,s9,p9 by A18, A24, AFF_1:11;
then x9,s9 // p9,q9 by A24, AFF_1:10;
then p9,q9 // r9,s9 by A13, A19, AFF_1:5;
hence contradiction by A7, Th36; :: thesis: verum

end;

r9,s9 // r9,x9 by A11, AFF_1:def 1;
then A25: r9,s9 // x9,r9 by AFF_1:4;
then r,s // x,r by Th36;
then a,b _|_ x,r by A12, A6, Def7;
then A26: x,r _|_ a,b by Def7;

A27: now :: thesis: ( x <> q implies not x <> r )

consider y9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A28: ( a9,b9 // q9,y9 & q9 <> y9 ) by DIRAF:40;
assume that
A29: x <> q and
A30: x <> r ; :: thesis: contradiction
not q9,y9 // x9,r9

proof

assume q9,y9 // x9,r9 ; :: thesis: contradiction
then q9,y9 // r9,s9 by A25, A30, AFF_1:5;
then r9,s9 // a9,b9 by A28, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def7;
hence contradiction by A7, Def7; :: thesis: verum

end;

then consider z9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A31: LIN q9,y9,z9 and
A32: LIN x9,r9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
q9,y9 // q9,z9 by A31, AFF_1:def 1;
then a9,b9 // q9,z9 by A28, AFF_1:5;
then A33: a,b // q,z by Th36;
A34: x9,r9 // x9,z9 by A32, AFF_1:def 1;
then x,r // x,z by Th36;
then a,b _|_ x,z by A26, A30, Def7;
then a,b _|_ q,z by A15, Def7;
then q,z _|_ q,z by A7, A33, Def7;
then x9,r9 // x9,q9 by A34, Def7;
then A35: LIN x9,r9,q9 by AFF_1:def 1;
( LIN x9,r9,x9 & LIN x9,q9,p9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,r9,p9 by A29, A35, AFF_1:11;
then x9,r9 // p9,q9 by A35, AFF_1:10;
then p9,q9 // r9,s9 by A25, A30, AFF_1:5;
hence contradiction by A7, Th36; :: thesis: verum

end;

p9,q9 // p9,x9 by A10, AFF_1:def 1;
then p9,q9 // x9,p9 by AFF_1:4;
then p,q // x,p by Th36;
then A36: a,b _|_ x,p by A9, A5, Def7;

A37: now :: thesis: ( x <> p implies not x <> s )

consider y9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A38: ( a9,b9 // p9,y9 & p9 <> y9 ) by DIRAF:40;
assume that
A39: x <> p and
A40: x <> s ; :: thesis: contradiction
not p9,y9 // x9,s9

proof

assume p9,y9 // x9,s9 ; :: thesis: contradiction
then p9,y9 // r9,s9 by A13, A40, AFF_1:5;
then r9,s9 // a9,b9 by A38, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def7;
hence contradiction by A7, Def7; :: thesis: verum

end;

then consider z9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A41: LIN p9,y9,z9 and
A42: LIN x9,s9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
p9,y9 // p9,z9 by A41, AFF_1:def 1;
then a9,b9 // p9,z9 by A38, AFF_1:5;
then A43: a,b // p,z by Th36;
A44: x9,s9 // x9,z9 by A42, AFF_1:def 1;
then x,s // x,z by Th36;
then a,b _|_ x,z by A14, A40, Def7;
then a,b _|_ p,z by A36, Def7;
then p,z _|_ p,z by A7, A43, Def7;
then x9,s9 // x9,p9 by A44, Def7;
then A45: LIN x9,s9,p9 by AFF_1:def 1;
( LIN x9,s9,x9 & LIN x9,p9,q9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,s9,q9 by A39, A45, AFF_1:11;
then x9,s9 // p9,q9 by A45, AFF_1:10;
then p9,q9 // r9,s9 by A13, A40, AFF_1:5;
hence contradiction by A7, Th36; :: thesis: verum

end;

now :: thesis: ( x <> p implies not x <> r )

consider y9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A46: ( a9,b9 // p9,y9 & p9 <> y9 ) by DIRAF:40;
assume that
A47: x <> p and
A48: x <> r ; :: thesis: contradiction
not p9,y9 // x9,r9

proof

assume p9,y9 // x9,r9 ; :: thesis: contradiction
then p9,y9 // r9,s9 by A25, A48, AFF_1:5;
then r9,s9 // a9,b9 by A46, AFF_1:5;
then r,s // a,b by Th36;
then a,b _|_ a,b by A12, A6, Def7;
hence contradiction by A7, Def7; :: thesis: verum

end;

then consider z9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A49: LIN p9,y9,z9 and
A50: LIN x9,r9,z9 by A1, AFF_1:60;
reconsider z = z9 as Element of POS ;
p9,y9 // p9,z9 by A49, AFF_1:def 1;
then a9,b9 // p9,z9 by A46, AFF_1:5;
then A51: a,b // p,z by Th36;
A52: x9,r9 // x9,z9 by A50, AFF_1:def 1;
then x,r // x,z by Th36;
then a,b _|_ x,z by A26, A48, Def7;
then a,b _|_ p,z by A36, Def7;
then p,z _|_ p,z by A7, A51, Def7;
then x9,r9 // x9,p9 by A52, Def7;
then A53: LIN x9,r9,p9 by AFF_1:def 1;
( LIN x9,r9,x9 & LIN x9,p9,q9 ) by A10, AFF_1:6, AFF_1:7;
then LIN x9,r9,q9 by A47, A53, AFF_1:11;
then x9,r9 // p9,q9 by A53, AFF_1:10;
then p9,q9 // r9,s9 by A25, A48, AFF_1:5;
hence contradiction by A7, Th36; :: thesis: verum

end;

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

end;

end;

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