let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS st a,b // c,d holds
b,a // c,d
let a, b, c, d be Element of SAS; :: thesis: ( a,b // c,d implies b,a // c,d )
assume A1: a,b // c,d ; :: thesis: b,a // c,d
a,b // b,a by Def1;
then ( a <> b implies b,a // c,d ) by A1, Def1;
hence b,a // c,d by A1; :: thesis: verum