let MP be OrtAfSp; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum