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 congr a,b,c,d ; :: thesis: congr c,d,a,b
then ( congr a,b,c,d & congr a,b,a,b ) by Th84;
hence congr c,d,a,b by Th85; :: thesis: verum