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:44;
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 19; :: 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:28; :: thesis: verum