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