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
let a, b, c, d be Element of SAS; :: thesis: ( congr a,b,c,d implies congr c,d,a,b )
assume A1: congr a,b,c,d ; :: thesis: congr c,d,a,b
congr a,b,a,b by Th84;
hence congr c,d,a,b by A1, Th85; :: thesis: verum