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_3) - (f `1_3)) <> (e `1_3) - (g `1_3) or (0. F) * ((e `2_3) - (f `2_3)) <> (e `2_3) - (g `2_3) or (0. F) * ((e `3_3) - (f `3_3)) <> (e `3_3) - (g `3_3) ) by Th2;
then A2: ( 0. F <> (e `1_3) - (g `1_3) or 0. F <> (e `2_3) - (g `2_3) or 0. F <> (e `3_3) - (g `3_3) ) ;
A3: f <> g

proof

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

end;

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