let FdSp be FanodesSp; for a, b, c, d, p, q, r, s being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s holds
c,d '||' r,s
let a, b, c, d, p, q, r, s be Element of FdSp; ( parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s implies c,d '||' r,s )
assume that
A1:
parallelogram a,p,b,q
and
A2:
parallelogram a,p,c,r
and
A3:
parallelogram b,q,d,s
; c,d '||' r,s
A4:
now ( not a,p,d are_collinear implies c,d '||' r,s )assume A5:
not
a,
p,
d are_collinear
;
c,d '||' r,s
parallelogram b,
q,
a,
p
by A1, Th33;
then
parallelogram a,
p,
d,
s
by A3, A5, Th40;
hence
c,
d '||' r,
s
by A2, Th39;
verum end;
A6:
now ( b,q,c are_collinear & a,p,d are_collinear implies c,d '||' r,s )A7:
a <> p
by A1, Th26;
A8:
( not
a,
p,
b are_collinear &
a,
p '||' a,
p )
by A1, PARSP_1:25;
assume that A9:
b,
q,
c are_collinear
and A10:
a,
p,
d are_collinear
;
c,d '||' r,s
a <> b
by A1, Th26;
then consider x being
Element of
FdSp such that A11:
a,
b,
x are_collinear
and A12:
x <> a
and A13:
x <> b
by Th38;
a,
b '||' a,
x
by A11;
then consider y being
Element of
FdSp such that A14:
parallelogram a,
p,
x,
y
by A12, A8, A7, Th11, Th34;
A15:
not
x,
y,
d are_collinear
by A10, A14, Th29;
parallelogram b,
q,
x,
y
by A1, A11, A13, A14, Th41;
then A16:
parallelogram x,
y,
d,
s
by A3, A15, Th40;
not
x,
y,
c are_collinear
by A1, A9, A11, A13, A14, Th29, Th41;
then
parallelogram x,
y,
c,
r
by A2, A14, Th40;
hence
c,
d '||' r,
s
by A16, Th39;
verum end;
now ( not b,q,c are_collinear implies c,d '||' r,s )assume
not
b,
q,
c are_collinear
;
c,d '||' r,sthen
parallelogram b,
q,
c,
r
by A1, A2, Th40;
hence
c,
d '||' r,
s
by A3, Th39;
verum end;
hence
c,d '||' r,s
by A4, A6; verum