let FdSp be FanodesSp; for a, b being Element of FdSp holds a,b congr a,b
let a, b be Element of FdSp; a,b congr a,b
now ( a <> b implies a,b congr a,b )assume
a <> b
;
a,b congr a,bthen consider p,
q being
Element of
FdSp such that A1:
parallelogram a,
b,
p,
q
by Th43;
parallelogram p,
q,
a,
b
by A1, Th33;
hence
a,
b congr a,
b
;
verum end;
hence
a,b congr a,b
; verum