let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS st congr a,b,c,d holds
( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a )
let a, b, c, d be Element of SAS; :: thesis: ( congr a,b,c,d implies ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a ) )
assume A1: congr a,b,c,d ; :: thesis: ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a )
then congr c,d,a,b ;
then A2: congr d,c,b,a by Th67;
( congr b,a,d,c & congr a,c,b,d ) by A1, Th67, Th68;
hence ( congr c,d,a,b & congr b,a,d,c & congr a,c,b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a ) by A2, Th67, Th68; :: thesis: verum