let SAS be Semi_Affine_Space; for a, b, c being Element of SAS ex d being Element of SAS st congr a,b,c,d
let a, b, c be Element of SAS; ex d being Element of SAS st congr a,b,c,d
A2:
now ( a <> b & a,b,c are_collinear implies ex d being Element of SAS st congr a,b,c,d )assume that A3:
a <> b
and A4:
a,
b,
c are_collinear
;
ex d being Element of SAS st congr a,b,c,dconsider p,
q being
Element of
SAS such that A5:
parallelogram a,
b,
p,
q
by A3, Lm1;
not
p,
q,
c are_collinear
by A4, A5, Th39;
then consider d being
Element of
SAS such that A6:
parallelogram p,
q,
c,
d
by Th44;
parallelogram p,
q,
a,
b
by A5, Th43;
then
congr a,
b,
c,
d
by A6;
hence
ex
d being
Element of
SAS st
congr a,
b,
c,
d
;
verum end;
now ( a <> b & not a,b,c are_collinear implies ex d being Element of SAS st congr a,b,c,d )assume that
a <> b
and A7:
not
a,
b,
c are_collinear
;
ex d being Element of SAS st congr a,b,c,d
ex
d being
Element of
SAS st
parallelogram a,
b,
c,
d
by A7, Th44;
hence
ex
d being
Element of
SAS st
congr a,
b,
c,
d
by Th60;
verum end;
hence
ex d being Element of SAS st congr a,b,c,d
by A1, A2; verum