let SAS be Semi_Affine_Space; for a, b, c, d being Element of SAS st congr a,b,c,d holds
congr a,c,b,d
let a, b, c, d be Element of SAS; ( congr a,b,c,d implies congr a,c,b,d )
assume A1:
congr a,b,c,d
; congr a,c,b,d
A2:
now assume A3:
a = c
;
congr a,c,b,d
congr a,
b,
a,
b
by Th84;
then
b = d
by A1, A3, Th81;
hence
congr a,
c,
b,
d
by A3, Def4;
verum end;
A4:
now assume that A5:
a <> b
and A6:
a <> c
and A7:
a,
b,
c is_collinear
;
congr a,c,b,dA8:
a,
b // a,
c
by A7, Def2;
consider p,
q being
Element of
SAS such that A9:
parallelogram p,
q,
a,
b
and A10:
parallelogram p,
q,
c,
d
by A1, A5, Def4;
A11:
a,
p // a,
p
by Th12;
( not
a,
b,
p is_collinear &
a <> p )
by A9, Th54, Th56;
then consider r being
Element of
SAS such that A12:
parallelogram a,
c,
p,
r
by A6, A8, A11, Th39, Th62;
A13:
a,
c // p,
r
by A12, Def3;
A14:
p,
q // c,
d
by A10, Def3;
(
p <> q &
p,
q // a,
b )
by A9, Def3, Th54;
then A15:
a,
b // c,
d
by A14, Def1;
then
a,
c // b,
d
by A5, A7, Th49;
then A16:
p,
r // b,
d
by A6, A13, Def1;
parallelogram p,
r,
a,
c
by A12, Th61;
then A17:
p,
a // r,
c
by Def3;
(
p,
a // q,
b &
p <> a )
by A9, Def3, Th54;
then A18:
r,
c // q,
b
by A17, Def1;
p,
c // q,
d
by A10, Def3;
then A19:
q,
d // p,
c
by Th17;
p,
q // a,
b
by A9, Def3;
then A20:
a,
b // p,
q
by Th17;
A21:
a,
c // p,
r
by A12, Def3;
a,
b // a,
c
by A7, Def2;
then
a,
c // p,
q
by A5, A20, Def1;
then
p,
q // p,
r
by A6, A21, Def1;
then A22:
r,
q // r,
p
by Th18;
a,
c,
b is_collinear
by A7, Th37;
then A23:
not
p,
r,
b is_collinear
by A12, Th57;
A24:
parallelogram p,
r,
a,
c
by A12, Th61;
c,
b // c,
d
by A5, A7, A15, Th50;
then
b,
c // b,
d
by Th18;
then
p,
b // r,
d
by A22, A18, A19, Def1;
then
parallelogram p,
r,
b,
d
by A23, A16, Def3;
hence
congr a,
c,
b,
d
by A24, Def4;
verum end;
A25:
now assume that
a <> b
and
a <> c
and A26:
not
a,
b,
c is_collinear
;
congr a,c,b,d
parallelogram a,
b,
c,
d
by A1, A26, Th78;
then
parallelogram a,
c,
b,
d
by Th61;
hence
congr a,
c,
b,
d
by Th79;
verum end;
hence
congr a,c,b,d
by A2, A4, A25; verum