let FdSp be FanodesSp; for a, b, c, d being Element of FdSp st a <> b & a,b,c are_collinear & a,b '||' c,d holds
a,c '||' b,d
let a, b, c, d be Element of FdSp; ( a <> b & a,b,c are_collinear & a,b '||' c,d implies a,c '||' b,d )
assume that
A1:
a <> b
and
A2:
a,b,c are_collinear
and
A3:
a,b '||' c,d
; a,c '||' b,d
now ( b <> c implies a,c '||' b,d )A4:
a,
b '||' a,
c
by A2;
then
a,
b '||' c,
b
by PARSP_1:24;
then
c,
b '||' c,
d
by A1, A3, PARSP_1:def 12;
then A5:
b,
c '||' b,
d
by PARSP_1:24;
assume A6:
b <> c
;
a,c '||' b,d
b,
c '||' a,
c
by A4, PARSP_1:24;
hence
a,
c '||' b,
d
by A6, A5, PARSP_1:def 12;
verum end;
hence
a,c '||' b,d
by A3; verum