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 & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a )
let a, b, c, d be Element of SAS; :: thesis: ( a,b // c,d implies ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a ) )
assume a,b // c,d ; :: thesis: ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a )
then c,d // a,b by Th2;
then A1: d,c // a,b by Th4;
then A2: d,c // b,a by Th5;
then c,d // b,a by Th4;
hence ( b,a // c,d & a,b // d,c & b,a // d,c & c,d // a,b & d,c // a,b & c,d // b,a & d,c // b,a ) by A1, A2, Th2, Th4; :: thesis: verum