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 x' = x, y' = y, z' = z as Element of (Af MP) by ANALMETR:47;
LIN x',y',z' by A1, ANALMETR:55;
then ( LIN x',z',y' & LIN y',x',z' & LIN y',z',x' & LIN z',x',y' & LIN z',y',x' ) by AFF_1:15;
hence ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) by ANALMETR:55; :: thesis: verum