let FdSp be FanodesSp; :: thesis: for o, a, b, p, q being Element of FdSp st o <> a & o <> b & o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear holds
a,b '||' p,q
let o, a, b, p, q be Element of FdSp; :: thesis: ( o <> a & o <> b & o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear implies a,b '||' p,q )
assume A1:
( o <> a & o <> b & o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear )
; :: thesis: a,b '||' p,q
A2:
now assume
o = p
;
:: thesis: a,b '||' p,qthen
(
p <> b &
p,
a '||' p,
b &
p,
b '||' p,
q )
by A1, Def2;
then
(
p <> b &
a,
b '||' p,
b &
p,
b '||' p,
q )
by PARSP_1:41;
hence
a,
b '||' p,
q
by PARSP_1:43;
:: thesis: verum end;
now assume
o <> p
;
:: thesis: a,b '||' p,qthen
(
o <> p &
o <> a &
o <> b &
o,
a '||' o,
b &
o,
a '||' o,
p &
o,
b '||' o,
q )
by A1, Def2;
then
(
o <> p &
o <> b &
o,
b '||' a,
b &
o,
b '||' o,
p &
o,
b '||' o,
q )
by PARSP_1:41, PARSP_1:def 12;
then
(
o <> p &
o <> b &
o,
b '||' a,
b &
o,
b '||' o,
p &
o,
p '||' o,
q )
by PARSP_1:def 12;
then
(
o <> p &
a,
b '||' o,
p &
o,
p '||' p,
q )
by PARSP_1:41, PARSP_1:def 12;
hence
a,
b '||' p,
q
by PARSP_1:43;
:: thesis: verum end;
hence
a,b '||' p,q
by A2; :: thesis: verum