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