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 A1: trap a,b,c,d,d ; :: thesis: d = b
then a,c // b,d by Def8;
then A2: d,b // a,c by Th17;
d,a,b is_collinear by A1, Def8;
then d,a // d,b by Def2;
then A3: d,b // a,d by Th17;
assume not d = b ; :: thesis: contradiction
then a,d // a,c by A3, A2, Def1;
then A4: d,a // d,c by Th18;
not d,a,c is_collinear by A1, Def8;
hence contradiction by A4, Def2; :: thesis: verum