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 Th13;
then d,c // a,b by Th15;
hence a,b // d,c by Th13; :: thesis: verum