let G be IncProjectivePlane; :: thesis: for a being POINT of G
for A, B being LINE of G st A <> B holds
( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) )
let a be POINT of G; :: thesis: for A, B being LINE of G st A <> B holds
( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) )
let A, B be LINE of G; :: thesis: ( A <> B implies ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) ) )
assume A1: A <> B ; :: thesis: ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) )
then A * B on A,B by Def9;
then A * B on B,A by Th1;
hence ( A * B on A & A * B on B & A * B = B * A ) by A1, Def2, Def9; :: thesis: ( a on A & a on B implies a = A * B )
assume ( a on A & a on B ) ; :: thesis: a = A * B
then a on A,B by Def2;
hence a = A * B by A1, Def9; :: thesis: verum