let FdSp be FanodesSp; for a, b, c, d, r, s being Element of FdSp st a,b congr c,d & a,b,c are_collinear & parallelogram r,s,a,b holds
parallelogram r,s,c,d
let a, b, c, d, r, s be Element of FdSp; ( a,b congr c,d & a,b,c are_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d )
assume that
A1:
a,b congr c,d
and
A2:
a,b,c are_collinear
and
A3:
parallelogram r,s,a,b
; parallelogram r,s,c,d
now ( a <> b implies parallelogram r,s,c,d )assume A4:
a <> b
;
parallelogram r,s,c,dthen consider p,
q being
Element of
FdSp such that A5:
parallelogram p,
q,
a,
b
and A6:
parallelogram p,
q,
c,
d
by A1;
(
r,
s '||' a,
b &
a,
b '||' c,
d )
by A1, A3, Th48;
then A7:
r,
s '||' c,
d
by A4, PARSP_1:26;
A8:
parallelogram a,
b,
r,
s
by A3, Th33;
parallelogram a,
b,
p,
q
by A5, Th33;
then A9:
r,
c '||' s,
d
by A6, A8, Th42;
not
r,
s,
c are_collinear
by A2, A3, Th29;
hence
parallelogram r,
s,
c,
d
by A7, A9;
verum end;
hence
parallelogram r,s,c,d
by A3, Th26; verum