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 ;
then A2: d,b // a,c by Th6;
d,a,b are_collinear by A1;
then d,a // d,b ;
then A3: d,b // a,d by Th6;
assume not d = b ; :: thesis: contradiction
then a,d // a,c by A3, A2, Def1;
then A4: d,a // d,c by Th7;
not d,a,c are_collinear by A1;
hence contradiction by A4; :: thesis: verum