let G be IncProjSp; :: thesis: for a, b, q, q1 being POINT of G st q on a * b & q on a * q1 & q <> a & q1 <> a & a <> b holds
q1 on a * b
let a, b, q, q1 be POINT of G; :: thesis: ( q on a * b & q on a * q1 & q <> a & q1 <> a & a <> b implies q1 on a * b )
assume that
A1: ( q on a * b & q on a * q1 & q <> a ) and
A2: q1 <> a and
A3: a <> b ; :: thesis: q1 on a * b
( a on a * b & a on a * q1 ) by A2, A3, Th16;
then a * b = a * q1 by A1, INCPROJ:def 4;
hence q1 on a * b by A2, Th16; :: thesis: verum