let FdSp be FanodesSp; for a, b, c, d being Element of FdSp st a,b congr c,d holds
a,b '||' c,d
let a, b, c, d be Element of FdSp; ( a,b congr c,d implies a,b '||' c,d )
assume A1:
a,b congr c,d
; a,b '||' c,d
now ( a <> b implies a,b '||' c,d )assume
a <> b
;
a,b '||' c,dthen consider p,
q being
Element of
FdSp such that A2:
parallelogram p,
q,
a,
b
and A3:
parallelogram p,
q,
c,
d
by A1;
A4:
p,
q '||' c,
d
by A3;
(
p <> q &
p,
q '||' a,
b )
by A2, Th26;
hence
a,
b '||' c,
d
by A4, PARSP_1:def 12;
verum end;
hence
a,b '||' c,d
by PARSP_1:20; verum