let F be Field; 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); 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:]; ( 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]] )
; ( 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
( (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; verum