let F be Field; :: thesis: for a, b being Element of (MPS F) holds a,b '||' b,a
let a, b be Element of (MPS F); :: thesis: a,b '||' b,a
consider e, f being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: [e,f,f,e] = [a,b,b,a] ;
A2: (((e `2) - (f `2)) * ((f `3) - (e `3))) - (((f `2) - (e `2)) * ((e `3) - (f `3))) = 0. F by Lm2;
( (((e `1) - (f `1)) * ((f `2) - (e `2))) - (((f `1) - (e `1)) * ((e `2) - (f `2))) = 0. F & (((e `1) - (f `1)) * ((f `3) - (e `3))) - (((f `1) - (e `1)) * ((e `3) - (f `3))) = 0. F ) by Lm2;
hence a,b '||' b,a by A1, A2, Th23; :: thesis: verum