let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d being Element of SAS st trap a,b,c,d,d holds
d = b
let a, b, c, d be Element of SAS; :: thesis: ( trap a,b,c,d,d implies d = b )
assume trap a,b,c,d,d ; :: thesis: d = b
then A1: ( not d,a,c is_collinear & d,a,b is_collinear & d,c,d is_collinear & a,c // b,d ) by Def8;
assume A2: not d = b ; :: thesis: contradiction
then ( d,a // d,b & a,c // b,d & d <> b ) by A1, Def2;
then ( d,b // a,d & d,b // a,c ) by Th17;
then a,d // a,c by A2, Def1;
then d,a // d,c by Th18;
hence contradiction by A1, Def2; :: thesis: verum