let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st congr a,b,c,d holds
a,b // c,d
let a, b, c, d be Element of SAS; ( congr a,b,c,d implies a,b // c,d )
assume A1:
congr a,b,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
SAS 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, Th36;
hence
a,
b // c,
d
by A4, Def1;
verum end;
hence
a,b // c,d
by Th3; verum