let FdSp be FanodesSp; :: thesis: for a, p, b, q, c, r, d, 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, p, b, q, c, r, d, s be Element of FdSp; :: thesis: ( parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s implies c,d '||' r,s )
assume A1:
( parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s )
; :: thesis: c,d '||' r,s
A2:
now assume
not
b,
q,
c is_collinear
;
:: thesis: c,d '||' r,sthen
(
parallelogram b,
q,
c,
r &
parallelogram b,
q,
d,
s )
by A1, Th48;
hence
c,
d '||' r,
s
by Th47;
:: thesis: verum end;
A3:
now assume
not
a,
p,
d is_collinear
;
:: thesis: c,d '||' r,sthen
( not
a,
p,
d is_collinear &
parallelogram b,
q,
a,
p &
parallelogram b,
q,
d,
s &
parallelogram a,
p,
c,
r )
by A1, Th41;
then
(
parallelogram a,
p,
d,
s &
parallelogram a,
p,
c,
r )
by Th48;
hence
c,
d '||' r,
s
by Th47;
:: thesis: verum end;
now assume A4:
(
b,
q,
c is_collinear &
a,
p,
d is_collinear )
;
:: thesis: c,d '||' r,s
a <> b
by A1, Th34;
then consider x being
Element of
FdSp such that A5:
(
a,
b,
x is_collinear &
x <> a &
x <> b )
by Th46;
A6:
a,
b '||' a,
x
by A5, Def2;
A7:
not
a,
p,
b is_collinear
by A1, Th36;
A8:
a,
p '||' a,
p
by PARSP_1:42;
a <> p
by A1, Th34;
then
not
a,
p,
x is_collinear
by A5, A6, A7, A8, Th17;
then consider y being
Element of
FdSp such that A9:
parallelogram a,
p,
x,
y
by Th42;
A10:
parallelogram b,
q,
x,
y
by A1, A5, A9, Th49;
then
( not
x,
y,
c is_collinear & not
x,
y,
d is_collinear )
by A4, A9, Th37;
then
(
parallelogram x,
y,
c,
r &
parallelogram x,
y,
d,
s )
by A1, A9, A10, Th48;
hence
c,
d '||' r,
s
by Th47;
:: thesis: verum end;
hence
c,d '||' r,s
by A2, A3; :: thesis: verum