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