let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, o being Element of SAS st trap a,b,c,d,o holds
trap c,d,a,b,o
let a, b, c, d, o be Element of SAS; :: thesis: ( trap a,b,c,d,o implies trap c,d,a,b,o )
assume A1: trap a,b,c,d,o ; :: thesis: trap c,d,a,b,o
then not o,a,c is_collinear by Def8;
then A2: not o,c,a is_collinear by Th37;
a,c // b,d by A1, Def8;
then A3: c,a // d,b by Th17;
( o,a,b is_collinear & o,c,d is_collinear ) by A1, Def8;
hence trap c,d,a,b,o by A2, A3, Def8; :: thesis: verum