let AS be AffinSpace; for a, a9, b, b9, o being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o holds
b9 = o
let a, a9, b, b9, o be Element of AS; ( not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o implies b9 = o )
assume that
A1:
not LIN o,a,b
and
A2:
LIN o,b,b9
and
A3:
a,b // a9,b9
and
A4:
a9 = o
; b9 = o
A5:
now not a,b // a9,bassume
a,
b // a9,
b
;
contradictionthen
b,
a // b,
a9
by Th3;
then
LIN b,
a,
a9
;
hence
contradiction
by A1, A4, Th5;
verum end;
a9,b // a9,b9
by A2, A4;
hence
b9 = o
by A3, A4, A5, Th4; verum