let SAS be Semi_Affine_Space; :: thesis: for o, p being Element of SAS st qtrap o,p holds
o <> p
let o, p be Element of SAS; :: thesis: ( qtrap o,p implies o <> p )
assume A1: qtrap o,p ; :: thesis: o <> p
assume A2: not o <> p ; :: thesis: contradiction
ex b being Element of SAS st o <> b

proof

consider x, y, z being Element of SAS such that
A3: ( x <> y & y <> z & z <> x ) by Th130;
( o <> x or o <> y or o <> z ) by A3;
hence ex b being Element of SAS st o <> b ; :: thesis: verum

end;

then consider b being Element of SAS such that
A4: o <> b ;
consider c being Element of SAS such that
A5: not o,b // o,c by A4, Th26;
consider d being Element of SAS such that
A6: ( o,p,b is_collinear implies ( o,c,d is_collinear & p,c // b,d ) ) by A1, Def9;
( o,o // o,b implies ( o,c // o,d & o,c // b,d ) ) by A2, A6, Def2;
then A7: ( ( b = d & not o,b // o,c & o,c // o,d ) or ( b <> d & o <> c & not o,b // o,c & o,c // o,d & o,c // b,d ) ) by A5, Def1, Th14;

now

assume A8: ( b <> d & not o,b // o,c & o,d // b,d & o,c // b,d ) ; :: thesis: ( b <> d & not o,b // o,c & b,d // o,b & b,d // o,c )
then d,o // d,b by Th17;
hence ( b <> d & not o,b // o,c & b,d // o,b & b,d // o,c ) by A8, Th17, Th18; :: thesis: verum

end;

hence contradiction by A7, Def1, Th17; :: thesis: verum