let MP be OrtAfSp; :: thesis: for x, y, z being Element of 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 ; :: 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 by ANALMETR:47;
A2: LIN x',y',z' by A1, ANALMETR:55;
then A3: ( LIN y',z',x' & LIN z',x',y' ) by AFF_1:15;
A4: LIN z',y',x' by A2, AFF_1:15;
( LIN x',z',y' & LIN y',x',z' ) by A2, 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 A3, A4, ANALMETR:55; :: thesis: verum