Proposition 8If two triangles have the two sides equal to two sides respectively, and have also the base equal to the base, they will also have the angle equal which are contained by the equal straight lines.
This proposition is essentially the side-side-side (SSS) property that says that if two triangles have three congruent sides then the respective angles of the triangles will be congruent also, therefore the triangles will be congruent.
In Nuprl, we define congruent triangles by the SSS property, so in our statement of this proposition we combine the assumptions of congruent sides into the 'Cong3(abc,xyz)'. We then set out to prove that the respective angles are congruent. Euclid's proof of this is similar to his proof of Proposition 4 in that he tried to justify his reasoning by applying triangles and showing that angles and sides will coincide.
Our proof of this proposition follows pretty easily from our definition of congruent angles, for which the definition and diagrammatic representation can be found here. To prove that two angles of these triangles are congruent we can use the degenerate case of our congruent angle definition, using the vertices of the original triangle as our "extended" points since we know that the segments making up the angle are already equal. Then we know that segment between those points are congruent because it is one of the original sides of the triangle, which we already know to be congruent.
Let ABC, DEF be two triangles having the two sides AB, AC equal to the two sides DE, DF respectively, namely AB to DE, and AC to DF; and let them have the base BC equal to the base EF; I say that the angle BAC is also equal to the angle EDF.
For, if the triangle ABC be applied to the triangle DEF, and if the point B be placed on the point E and the straight line BC on EF, the point C will also coincide with F, because BC is equal to EF.
Then, BC coinciding with EF, BA, AC will also coincide with ED, DF; for, if the base BC coincides with the base EF, and the sides BA, AC do not coincide with ED, DF but fall beside them as EG, GF.
Then, given two straight lines constructed on a straight line [from its extremities] and meeting in a point, there will have been constructed on the same straight line [from its extremities], and on the same side of it, two other straight lines meeting in another point and equal to the former two respectively, namely each to that which has the same extremity with it.
But they cannot be so constructed. [1.7]Given two straight lines constructed on a straight linee [from its extremities] and meeting in a point, there cannot be constructed on the same straight line [from its extremities], and on the same side of it, two other straight lines meeting in another point and equal to the former two respectively, namely each to that which has the same extremity with it.
Therefore it is not possible that, if the base BC be applied to the base EF, the sides B0A, AC should not coincide with ED, DF; they will therefore coincide, so that the angle BAC will also coincide with the angle EDF, and will be equal to it.
If therefore etc.
Proof in Nuprl