let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ex d being Element of SAS st congr a,b,c,d
A1: now :: thesis: ( a = b implies ex d being Element of SAS st congr a,b,c,d )
assume a = b ; :: thesis: ex d being Element of SAS st congr a,b,c,d
then congr a,b,c,c ;
hence ex d being Element of SAS st congr a,b,c,d ; :: thesis: verum
end;
A2: now :: thesis: ( 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 ; :: thesis: ex d being Element of SAS st congr a,b,c,d
consider 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 ; :: thesis: verum
end;
now :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
hence ex d being Element of SAS st congr a,b,c,d by A1, A2; :: thesis: verum