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