let S be OAffinSpace; for x, y, z, t being Element of S st x,y,z are_collinear & x,y,t are_collinear holds
x,y '||' z,t
let x, y, z, t be Element of S; ( x,y,z are_collinear & x,y,t are_collinear implies x,y '||' z,t )
assume A1:
( x,y,z are_collinear & x,y,t are_collinear )
; x,y '||' z,t
now ( x <> y implies x,y '||' z,t )A2:
(
x,
y '||' x,
z &
x,
y '||' x,
t )
by A1;
assume
x <> y
;
x,y '||' z,tthen
x,
z '||' x,
t
by A2, Th23;
then
z,
x '||' z,
t
by Th21;
then
x,
z '||' z,
t
by Th22;
hence
x,
y '||' z,
t
by A2, Th23;
verum end;
hence
x,y '||' z,t
by Th20; verum