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 )
let x, y, z be Element of AS; :: thesis: ( LIN x,y,z implies ( LIN x,z,y & LIN y,x,z ) )
assume LIN x,y,z ; :: thesis: ( LIN x,z,y & LIN y,x,z )
then A1: x,y // x,z by Def1;
then A2: y,x // y,z by DIRAF:40;
x,z // x,y by A1, Th13;
hence ( LIN x,z,y & LIN y,x,z ) by A2, Def1; :: thesis: verum