let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st congr a,b,c,d holds
congr b,a,d,c
let a, b, c, d be Element of SAS; ( congr a,b,c,d implies congr b,a,d,c )
assume A1:
congr a,b,c,d
; congr b,a,d,c
A2:
now ( a <> b implies congr b,a,d,c )assume
a <> b
;
congr b,a,d,cthen consider p,
q being
Element of
SAS such that A3:
(
parallelogram p,
q,
a,
b &
parallelogram p,
q,
c,
d )
by A1;
(
parallelogram q,
p,
b,
a &
parallelogram q,
p,
d,
c )
by A3, Th43;
hence
congr b,
a,
d,
c
;
verum end;
( a = b implies congr b,a,d,c )
by A1, Th54;
hence
congr b,a,d,c
by A2; verum