let POS be non empty ParOrtStr ; :: thesis:
set P = AffinStruct(# the carrier of POS, the CONGR of POS #);

hereby :: thesis:

assume A1: POS is OrtAfPl-like ; :: thesis:
then AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane ;
hence ex x, y being Element of POS st x <> y by DIRAF:46; :: thesis:
let a, b, c, d, p, q, r, s be Element of POS; :: thesis:
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q, r9 = r, s9 = s as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
consider x9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A2: ( a9,b9 // c9,x9 & a9,c9 // b9,x9 ) by A1, DIRAF:46;
( a9,b9 // b9,a9 & a9,b9 // c9,c9 ) by A1, DIRAF:46;
hence ( a,b // b,a & a,b // c,c ) by Th36; :: thesis:

hereby :: thesis:

assume ( a,b // p,q & a,b // r,s ) ; :: thesis:
then ( a9,b9 // p9,q9 & a9,b9 // r9,s9 ) by Th36;
then ( p9,q9 // r9,s9 or a9 = b9 ) by A1, DIRAF:46;
hence ( p,q // r,s or a = b ) by Th36; :: thesis:

end;

hereby :: thesis:

assume a,b // a,c ; :: thesis:
then a9,b9 // a9,c9 by Th36;
then b9,a9 // b9,c9 by A1, DIRAF:46;
hence b,a // b,c by Th36; :: thesis:

end;

reconsider x = x9 as Element of POS ;
consider x9, y9, z9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A3: not x9,y9 // x9,z9 by A1, DIRAF:46;
( a,b // c,x & a,c // b,x ) by A2, Th36;
hence ex x being Element of POS st
( a,b // c,x & a,c // b,x ) ; :: thesis:
reconsider x = x9, y = y9, z = z9 as Element of POS ;
consider x9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A4: a9,b9 // c9,x9 and
A5: c9 <> x9 by A1, DIRAF:46;
not x,y // x,z by A3, Th36;
hence not for x, y, z being Element of POS holds x,y // x,z ; :: thesis:
reconsider x = x9 as Element of POS ;
a,b // c,x by A4, Th36;
hence ex x being Element of POS st
( a,b // c,x & c <> x ) by A5; :: thesis:

hereby :: thesis:

assume that
A6: a,b // b,d and
A7: b <> a ; :: thesis:
a9,b9 // b9,d9 by A6, Th36;
then consider x9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A8: ( c9,b9 // b9,x9 & c9,a9 // d9,x9 ) by A1, A7, DIRAF:46;
reconsider x = x9 as Element of POS ;
( c,b // b,x & c,a // d,x ) by A8, Th36;
hence ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ; :: thesis:

end;

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 ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) ) by A1; :: thesis:
assume not a,b // c,d ; :: thesis:
then not a9,b9 // c9,d9 by Th36;
then consider x9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A9: ( a9,b9 // a9,x9 & c9,d9 // c9,x9 ) by A1, DIRAF:46;
reconsider x = x9 as Element of POS ;
( a,b // a,x & c,d // c,x ) by A9, Th36;
hence ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ; :: thesis:

end;

given a, b being Element of POS such that A10: a <> b ; :: thesis:
assume A11: for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( 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 ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ; :: thesis:

A12: now :: thesis:

let x, y, z be Element of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis:
reconsider x9 = x, y9 = y, z9 = z as Element of POS ;
consider t9 being Element of POS such that
A13: x9,z9 // y9,t9 and
A14: y9 <> t9 by A11;
reconsider t = t9 as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
x,z // y,t by A13, Th36;
hence ex t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,z // y,t & y <> t ) by A14; :: thesis:

end;

A15: now :: thesis:

let x, y, z, t, u, w be Element of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis:
reconsider a = x, b = y, c = z, d = t, e = u, f = w as Element of POS ;
( a,b // b,a & a,b // c,c ) by A11;
hence ( x,y // y,x & x,y // z,z ) by Th36; :: thesis:
thus ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) :: thesis:

proof

assume that
A16: x <> y and
A17: ( x,y // z,t & x,y // u,w ) ; :: thesis:
( a,b // c,d & a,b // e,f ) by A17, Th36;
then c,d // e,f by A11, A16;
hence z,t // u,w by Th36; :: thesis:

end;

thus ( x,y // x,z implies y,x // y,z ) :: thesis:

proof

assume x,y // x,z ; :: thesis:
then a,b // a,c by Th36;
then b,a // b,c by A11;
hence y,x // y,z by Th36; :: thesis:

end;

A18: now :: thesis:

let x, y, z, t be Element of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis:
assume A19: not x,y // z,t ; :: thesis:
reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS ;
not x9,y9 // z9,t9 by A19, Th36;
then consider u9 being Element of POS such that
A20: ( x9,y9 // x9,u9 & z9,t9 // z9,u9 ) by A11;
reconsider u = u9 as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
( x,y // x,u & z,t // z,u ) by A20, Th36;
hence ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,y // x,u & z,t // z,u ) ; :: thesis:

end;

A21: now :: thesis:

let x, y, z, t be Element of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis:
assume that
A22: z,x // x,t and
A23: x <> z ; :: thesis:
reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS ;
z9,x9 // x9,t9 by A22, Th36;
then consider u9 being Element of POS such that
A24: ( y9,x9 // x9,u9 & y9,z9 // t9,u9 ) by A11, A23;
reconsider u = u9 as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
( y,x // x,u & y,z // t,u ) by A24, Th36;
hence ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( y,x // x,u & y,z // t,u ) ; :: thesis:

end;

A25: now :: thesis:

let x, y, z be Element of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis:
reconsider x9 = x, y9 = y, z9 = z as Element of POS ;
consider t9 being Element of POS such that
A26: ( x9,y9 // z9,t9 & x9,z9 // y9,t9 ) by A11;
reconsider t = t9 as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
( x,y // z,t & x,z // y,t ) by A26, Th36;
hence ex t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,y // z,t & x,z // y,t ) ; :: thesis:

end;

not for x, y, z being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) holds x,y // x,z

proof

consider x, y, z being Element of POS such that
A27: not x,y // x,z by A11;
reconsider x9 = x, y9 = y, z9 = z as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
not x9,y9 // x9,z9 by A27, Th36;
hence not for x, y, z being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) holds x,y // x,z ; :: thesis:

end;

hence AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane by A10, A15, A12, A25, A21, A18, DIRAF:46; :: according to ANALMETR:def 9 :: thesis:
thus 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 ) ) by A11; :: thesis:
thus for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) by A11; :: thesis: