let AS be AffinSpace; :: thesis: for x, y being Element of AS holds
( LIN x,x,y & LIN x,y,y & LIN x,y,x )
let x, y be Element of AS; :: thesis: ( LIN x,x,y & LIN x,y,y & LIN x,y,x )
A1: x,y // x,y by Th11;
A2: x,y // x,x by Th12;
x,x // x,y by Th12;
hence ( LIN x,x,y & LIN x,y,y & LIN x,y,x ) by A1, A2, Def1; :: thesis: verum