let MP be OrtAfSp; for x, y, z being Element of MP st LIN x,y,z holds
( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
let x, y, z be Element of MP; ( LIN x,y,z implies ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) )
assume A1:
LIN x,y,z
; ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
reconsider x9 = x, y9 = y, z9 = z as Element of AffinStruct(# the carrier of MP, the CONGR of MP #) ;
A2:
LIN x9,y9,z9
by A1, ANALMETR:40;
then A3:
( LIN y9,z9,x9 & LIN z9,x9,y9 )
by AFF_1:6;
A4:
LIN z9,y9,x9
by A2, AFF_1:6;
( LIN x9,z9,y9 & LIN y9,x9,z9 )
by A2, AFF_1:6;
hence
( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x )
by A3, A4, ANALMETR:40; verum