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