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 )
ex b being Element of SAS st o <> b
proof
consider x, y, z being Element of SAS such that
A1: x <> y and
y <> z and
z <> x by Th102;
( o <> x or o <> y or o <> z ) by A1;
hence ex b being Element of SAS st o <> b ; :: thesis: verum
end;
then consider b being Element of SAS such that
A2: o <> b ;
consider c being Element of SAS such that
A3: not o,b // o,c by A2, Th13;
assume qtrap o,p ; :: thesis: o <> p
then consider d being Element of SAS such that
A4: ( o,p,b are_collinear implies ( o,c,d are_collinear & p,c // b,d ) ) ;
A5: now :: thesis: ( b <> d & not o,b // o,c & o,d // b,d & o,c // b,d implies ( b <> d & not o,b // o,c & b,d // o,b & b,d // o,c ) )
assume that
A6: ( b <> d & not o,b // o,c ) and
A7: o,d // b,d and
A8: o,c // b,d ; :: thesis: ( b <> d & not o,b // o,c & b,d // o,b & b,d // o,c )
d,o // d,b by A7, Th6;
hence ( b <> d & not o,b // o,c & b,d // o,b & b,d // o,c ) by A6, A8, Th6, Th7; :: thesis: verum
end;
assume not o <> p ; :: thesis: contradiction
then ( o,o // o,b implies ( o,c // o,d & o,c // b,d ) ) by A4;
then ( ( 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 A3, Def1, Th3;
hence contradiction by A5, Def1, Th6; :: thesis: verum