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 ( a = c implies congr a,c,b,d )assume A3:
a = c
;
congr a,c,b,d
congr a,
b,
a,
b
by Th64;
then
b = d
by A1, A3, Th62;
hence
congr a,
c,
b,
d
by A3;
verum end;
A4:
now ( a <> b & a <> c & a,b,c are_collinear implies congr a,c,b,d )assume that A5:
a <> b
and A6:
a <> c
and A7:
a,
b,
c are_collinear
;
congr a,c,b,dA8:
a,
b // a,
c
by A7;
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;
A11:
a,
p // a,
p
by Th1;
( not
a,
b,
p are_collinear &
a <> p )
by A9, Th36, Th38;
then consider r being
Element of
SAS such that A12:
parallelogram a,
c,
p,
r
by A6, A8, A11, Th23, Th44;
A13:
a,
c // p,
r
by A12;
A14:
p,
q // c,
d
by A10;
(
p <> q &
p,
q // a,
b )
by A9, Th36;
then A15:
a,
b // c,
d
by A14, Def1;
then
a,
c // b,
d
by A5, A7, Th32;
then A16:
p,
r // b,
d
by A6, A13, Def1;
parallelogram p,
r,
a,
c
by A12, Th43;
then A17:
p,
a // r,
c
;
(
p,
a // q,
b &
p <> a )
by A9, Th36;
then A18:
r,
c // q,
b
by A17, Def1;
p,
c // q,
d
by A10;
then A19:
q,
d // p,
c
by Th6;
p,
q // a,
b
by A9;
then A20:
a,
b // p,
q
by Th6;
A21:
a,
c // p,
r
by A12;
a,
b // a,
c
by A7;
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 Th7;
a,
c,
b are_collinear
by A7, Th22;
then A23:
not
p,
r,
b are_collinear
by A12, Th39;
A24:
parallelogram p,
r,
a,
c
by A12, Th43;
c,
b // c,
d
by A5, A7, A15, Th33;
then
b,
c // b,
d
by Th7;
then
p,
b // r,
d
by A22, A18, A19, Def1;
then
parallelogram p,
r,
b,
d
by A23, A16;
hence
congr a,
c,
b,
d
by A24;
verum end;
A25:
now ( a <> b & a <> c & not a,b,c are_collinear implies congr a,c,b,d )assume that
a <> b
and
a <> c
and A26:
not
a,
b,
c are_collinear
;
congr a,c,b,d
parallelogram a,
b,
c,
d
by A1, A26, Th59;
then
parallelogram a,
c,
b,
d
by Th43;
hence
congr a,
c,
b,
d
by Th60;
verum end;
hence
congr a,c,b,d
by A2, A4, A25; verum