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

hereby :: thesis:

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

end;

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

hereby :: thesis:

assume ( a,b // b,d & b <> a ) ; :: thesis:
then ( a',b' // b',d' & b' <> a' ) by Th48;
then consider x' being Element of (Af POS) such that
A6: ( c',b' // b',x' & c',a' // d',x' ) by A2, DIRAF:54;
reconsider x = x' as Element of POS ;
( c,b // b,x & c,a // d,x ) by A6, Th48;
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, Def10; :: thesis:
assume not a,b // c,d ; :: thesis:
then not a',b' // c',d' by Th48;
then consider x' being Element of the carrier of (Af POS) such that
A7: ( a',b' // a',x' & c',d' // c',x' ) by A2, DIRAF:54;
reconsider x = x' as Element of POS ;
( a,b // a,x & c,d // c,x ) by A7, Th48;
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 A8: a <> b ; :: thesis:
assume A9: 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:

A10: now

let x, y, z, t, u, w be Element of (Af POS); :: thesis:
reconsider a = x, b = y, c = z, d = t, e = u, f = w as Element of POS ;
thus ( x,y // y,x & x,y // z,z ) :: thesis:

proof

( a,b // b,a & a,b // c,c ) by A9;
hence ( x,y // y,x & x,y // z,z ) by Th48; :: thesis:

end;

thus ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) :: thesis:

proof

assume ( x <> y & x,y // z,t & x,y // u,w ) ; :: thesis:
then ( a,b // c,d & a,b // e,f & a <> b ) by Th48;
then c,d // e,f by A9;
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 A9;
hence y,x // y,z by Th48; :: thesis:

end;

A11: not for x, y, z being Element of (Af POS) holds x,y // x,z

proof

consider x, y, z being Element of POS such that
A12: not x,y // x,z by A9;
reconsider x' = x, y' = y, z' = z as Element of (Af POS) ;
not x',y' // x',z' by A12, Th48;
hence not for x, y, z being Element of (Af POS) holds x,y // x,z ; :: thesis:

end;

A13: now

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

end;

A15: now

let x, y, z be Element of (Af POS); :: thesis:
reconsider x' = x, y' = y, z' = z as Element of POS ;
consider t' being Element of POS such that
A16: ( x',y' // z',t' & x',z' // y',t' ) by A9;
reconsider t = t' as Element of the carrier of (Af POS) ;
( x,y // z,t & x,z // y,t ) by A16, Th48;
hence ex t being Element of (Af POS) st
( x,y // z,t & x,z // y,t ) ; :: thesis:

end;

A17: now

let x, y, z, t be Element of (Af POS); :: thesis:
assume A18: ( z,x // x,t & x <> z ) ; :: thesis:
reconsider x' = x, y' = y, z' = z, t' = t as Element of the carrier of POS ;
( z',x' // x',t' & x' <> z' ) by A18, Th48;
then consider u' being Element of POS such that
A19: ( y',x' // x',u' & y',z' // t',u' ) by A9;
reconsider u = u' as Element of (Af POS) ;
( y,x // x,u & y,z // t,u ) by A19, Th48;
hence ex u being Element of (Af POS) st
( y,x // x,u & y,z // t,u ) ; :: thesis:

end;

now

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

end;

hence AffinStruct(# the carrier of POS,the CONGR of POS #) is AffinPlane by A8, A10, A11, A13, A15, A17, DIRAF:54; :: according to ANALMETR:def 10 :: 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 A9; :: thesis:
thus for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) by A9; :: thesis: