let AS be AffinSpace; :: thesis: for x, y, z being Element of AS 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 AS; :: 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 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 )
hence ( LIN x,z,y & LIN y,x,z ) by Lm4; :: thesis: ( LIN y,z,x & LIN z,x,y & LIN z,y,x )
hence ( LIN y,z,x & LIN z,x,y ) by Lm4; :: thesis: LIN z,y,x
hence LIN z,y,x by Lm4; :: thesis: verum