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 ;

hence ( A * B on A & A * B on B & A * B = B * A ) by A1, 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 ;

hence a = A * B by A1, Def9; :: thesis: verum

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 ;

hence ( A * B on A & A * B on B & A * B = B * A ) by A1, 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 ;

hence a = A * B by A1, Def9; :: thesis: verum