let F be Field; :: thesis: for a, b, c being Element of (MPS F)
for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] holds
( e <> f & e <> g & f <> g )
let a, b, c be Element of (MPS F); :: thesis: for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] holds
( e <> f & e <> g & f <> g )
let e, f, g be Element of [: the carrier of F, the carrier of F, the carrier of F:]; :: thesis: ( not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] implies ( e <> f & e <> g & f <> g ) )
assume A1: ( not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] ) ; :: thesis: ( e <> f & e <> g & f <> g )
then ( (0. F) * ((e `1) - (f `1)) <> (e `1) - (g `1) or (0. F) * ((e `2) - (f `2)) <> (e `2) - (g `2) or (0. F) * ((e `3) - (f `3)) <> (e `3) - (g `3) ) by Th2;
then A2: ( 0. F <> (e `1) - (g `1) or 0. F <> (e `2) - (g `2) or 0. F <> (e `3) - (g `3) ) by VECTSP_1:12;
A3: f <> g

proof

assume A4: not f <> g ; :: thesis: contradiction
( ((e `1) - (f `1)) * (1_ F) <> (e `1) - (g `1) or ((e `2) - (f `2)) * (1_ F) <> (e `2) - (g `2) or ((e `3) - (f `3)) * (1_ F) <> (e `3) - (g `3) ) by A1, Th2;
hence contradiction by A4, VECTSP_1:def 8; :: thesis: verum

end;

( (e `1) - (f `1) <> 0. F or (e `2) - (f `2) <> 0. F or (e `3) - (f `3) <> 0. F ) by A1, Th2;
hence ( e <> f & e <> g & f <> g ) by A2, A3, RLVECT_1:15; :: thesis: verum