let POS be non empty ParOrtStr ; :: thesis:
set P = Af POS;

hereby :: thesis:

assume A1: POS is OrtAfPl-like ; :: thesis:
then Af POS is AffinPlane ;
hence ex x, y being Element of st x <> y by DIRAF:54; :: thesis:
let a, b, c, d, p, q, r, s be Element of ; :: thesis:
reconsider a' = a, b' = b, c' = c, d' = d, p' = p, q' = q, r' = r, s' = s as Element of ;
consider x' being Element of such that
A2: ( a',b' // c',x' & a',c' // b',x' ) by A1, DIRAF:54;
( a',b' // b',a' & a',b' // c',c' ) by A1, DIRAF:54;
hence ( a,b // b,a & a,b // c,c ) by Th48; :: thesis:

hereby :: thesis:

assume ( a,b // p,q & a,b // r,s ) ; :: thesis:
then ( a',b' // p',q' & a',b' // r',s' ) by Th48;
then ( p',q' // r',s' or a' = b' ) by A1, DIRAF:54;
hence ( p,q // r,s or a = b ) by Th48; :: thesis:

end;

hereby :: thesis:

assume a,b // a,c ; :: thesis:
then a',b' // a',c' by Th48;
then b',a' // b',c' by A1, DIRAF:54;
hence b,a // b,c by Th48; :: thesis:

end;

reconsider x = x' as Element of ;
consider x', y', z' being Element of such that
A3: not x',y' // x',z' by A1, DIRAF:54;
( a,b // c,x & a,c // b,x ) by A2, Th48;
hence ex x being Element of st
( a,b // c,x & a,c // b,x ) ; :: thesis:
reconsider x = x', y = y', z = z' as Element of ;
consider x' being Element of such that
A4: a',b' // c',x' and
A5: c' <> x' by A1, DIRAF:54;
not x,y // x,z by A3, Th48;
hence not for x, y, z being Element of holds x,y // x,z ; :: thesis:
reconsider x = x' as Element of ;
a,b // c,x by A4, Th48;
hence ex x being Element of st
( a,b // c,x & c <> x ) by A5; :: thesis:

hereby :: thesis:

assume that
A6: a,b // b,d and
A7: b <> a ; :: thesis:
a',b' // b',d' by A6, Th48;
then consider x' being Element of such that
A8: ( c',b' // b',x' & c',a' // d',x' ) by A1, A7, DIRAF:54;
reconsider x = x' as Element of ;
( c,b // b,x & c,a // d,x ) by A8, Th48;
hence ex x being Element of 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 st
( a,b _|_ c,x & c <> x ) ) by A1, Def10; :: thesis:
assume not a,b // c,d ; :: thesis:
then not a',b' // c',d' by Th48;
then consider x' being Element of such that
A9: ( a',b' // a',x' & c',d' // c',x' ) by A1, DIRAF:54;
reconsider x = x' as Element of ;
( a,b // a,x & c,d // c,x ) by A9, Th48;
hence ex x being Element of st
( a,b // a,x & c,d // c,x ) ; :: thesis:

end;

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

A12: now

let x, y, z be Element of ; :: thesis:
reconsider x' = x, y' = y, z' = z as Element of ;
consider t' being Element of such that
A13: x',z' // y',t' and
A14: y' <> t' by A11;
reconsider t = t' as Element of ;
x,z // y,t by A13, Th48;
hence ex t being Element of st
( x,z // y,t & y <> t ) by A14; :: thesis:

end;

A15: now

let x, y, z, t, u, w be Element of ; :: thesis:
reconsider a = x, b = y, c = z, d = t, e = u, f = w as Element of ;
( a,b // b,a & a,b // c,c ) by A11;
hence ( x,y // y,x & x,y // z,z ) by Th48; :: 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, Th48;
then c,d // e,f by A11, A16;
hence z,t // u,w by Th48; :: 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 Th48;
then b,a // b,c by A11;
hence y,x // y,z by Th48; :: thesis:

end;

A18: now

let x, y, z, t be Element of ; :: thesis:
assume A19: not x,y // z,t ; :: thesis:
reconsider x' = x, y' = y, z' = z, t' = t as Element of ;
not x',y' // z',t' by A19, Th48;
then consider u' being Element of such that
A20: ( x',y' // x',u' & z',t' // z',u' ) by A11;
reconsider u = u' as Element of ;
( x,y // x,u & z,t // z,u ) by A20, Th48;
hence ex u being Element of st
( x,y // x,u & z,t // z,u ) ; :: thesis:

end;

A21: now

let x, y, z, t be Element of ; :: thesis:
assume that
A22: z,x // x,t and
A23: x <> z ; :: thesis:
reconsider x' = x, y' = y, z' = z, t' = t as Element of ;
z',x' // x',t' by A22, Th48;
then consider u' being Element of such that
A24: ( y',x' // x',u' & y',z' // t',u' ) by A11, A23;
reconsider u = u' as Element of ;
( y,x // x,u & y,z // t,u ) by A24, Th48;
hence ex u being Element of st
( y,x // x,u & y,z // t,u ) ; :: thesis:

end;

A25: now

let x, y, z be Element of ; :: thesis:
reconsider x' = x, y' = y, z' = z as Element of ;
consider t' being Element of such that
A26: ( x',y' // z',t' & x',z' // y',t' ) by A11;
reconsider t = t' as Element of ;
( x,y // z,t & x,z // y,t ) by A26, Th48;
hence ex t being Element of st
( x,y // z,t & x,z // y,t ) ; :: thesis:

end;

not for x, y, z being Element of holds x,y // x,z

proof

consider x, y, z being Element of such that
A27: not x,y // x,z by A11;
reconsider x' = x, y' = y, z' = z as Element of ;
not x',y' // x',z' by A27, Th48;
hence not for x, y, z being Element of 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:54; :: according to ANALMETR:def 10 :: thesis:
thus for a, b, c, d, p, q, r, s being Element of 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 ex x being Element of st
( a,b _|_ c,x & c <> x ) by A11; :: thesis: