let FdSp be FanodesSp; :: thesis: for a, b, c, d, r, s being Element of FdSp st r,s congr a,b & r,s congr c,d holds
a,b congr c,d
let a, b, c, d, r, s be Element of FdSp; :: thesis: ( r,s congr a,b & r,s congr c,d implies a,b congr c,d )
assume that
A1: r,s congr a,b and
A2: r,s congr c,d ; :: thesis: a,b congr c,d
A3: now :: thesis: ( r <> s & not r,s,a are_collinear & not r,s,c are_collinear implies a,b congr c,d )
assume that
r <> s and
A4: ( not r,s,a are_collinear & not r,s,c are_collinear ) ; :: thesis: a,b congr c,d
( parallelogram r,s,a,b & parallelogram r,s,c,d ) by A1, A2, A4, Th50;
hence a,b congr c,d ; :: thesis: verum
end;
A5: now :: thesis: ( r <> s & r,s,c are_collinear implies a,b congr c,d )
assume that
A6: r <> s and
A7: r,s,c are_collinear ; :: thesis: a,b congr c,d
consider p, q being Element of FdSp such that
A8: parallelogram p,q,r,s and
A9: parallelogram p,q,a,b by A1, A6;
parallelogram p,q,c,d by A2, A7, A8, Th52;
hence a,b congr c,d by A9; :: thesis: verum
end;
A10: now :: thesis: ( r <> s & r,s,a are_collinear implies a,b congr c,d )
assume that
A11: r <> s and
A12: r,s,a are_collinear ; :: thesis: a,b congr c,d
consider p, q being Element of FdSp such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2, A11;
parallelogram p,q,a,b by A1, A12, A13, Th52;
hence a,b congr c,d by A14; :: thesis: verum
end;
( r = s implies a,b congr c,d ) by A1, A2, Th45;
hence a,b congr c,d by A10, A5, A3; :: thesis: verum