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 trap a,b,c,d,o ; :: thesis: trap c,d,a,b,o
then ( not o,a,c is_collinear & o,a,b is_collinear & o,c,d is_collinear & a,c // b,d ) by Def8;
then ( not o,c,a is_collinear & o,a,b is_collinear & o,c,d is_collinear & c,a // d,b ) by Th17, Th37;
hence trap c,d,a,b,o by Def8; :: thesis: verum