let SAS be Semi_Affine_Space; for a, a9, b, b9, c, c9, d, d9 being Element of SAS st parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 holds
c,d // c9,d9
let a, a9, b, b9, c, c9, d, d9 be Element of SAS; ( parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 implies c,d // c9,d9 )
assume that
A1:
parallelogram a,a9,b,b9
and
A2:
parallelogram a,a9,c,c9
and
A3:
parallelogram b,b9,d,d9
; c,d // c9,d9
A4:
now ( not a,a9,d are_collinear implies c,d // c9,d9 )assume A5:
not
a,
a9,
d are_collinear
;
c,d // c9,d9
parallelogram b,
b9,
a,
a9
by A1, Th43;
then
parallelogram a,
a9,
d,
d9
by A3, A5, Th50;
hence
c,
d // c9,
d9
by A2, Th49;
verum end;
A6:
now ( b,b9,c are_collinear & a,a9,d are_collinear implies c,d // c9,d9 )A7:
( not
a,
a9,
b are_collinear &
a,
a9 // a,
a9 )
by A1, Th1;
A8:
a <> a9
by A1, Th36;
assume that A9:
b,
b9,
c are_collinear
and A10:
a,
a9,
d are_collinear
;
c,d // c9,d9
a <> b
by A1, Th36;
then consider x being
Element of
SAS such that A11:
a,
b,
x are_collinear
and A12:
x <> a
and A13:
x <> b
by Th48;
a,
b // a,
x
by A11;
then consider y being
Element of
SAS such that A14:
parallelogram a,
a9,
x,
y
by A12, A7, A8, Th23, Th44;
A15:
not
x,
y,
d are_collinear
by A10, A14, Th39;
parallelogram b,
b9,
x,
y
by A1, A11, A13, A14, Th51;
then A16:
parallelogram x,
y,
d,
d9
by A3, A15, Th50;
not
x,
y,
c are_collinear
by A1, A9, A11, A13, A14, Th39, Th51;
then
parallelogram x,
y,
c,
c9
by A2, A14, Th50;
hence
c,
d // c9,
d9
by A16, Th49;
verum end;
now ( not b,b9,c are_collinear implies c,d // c9,d9 )assume
not
b,
b9,
c are_collinear
;
c,d // c9,d9then
parallelogram b,
b9,
c,
c9
by A1, A2, Th50;
hence
c,
d // c9,
d9
by A3, Th49;
verum end;
hence
c,d // c9,d9
by A4, A6; verum