let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of st a,b // c,d holds
b,a // c,d
let a, b, c, d be Element of ; :: 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