let G be IncProjSp; :: thesis: for a, b being POINT of G

for L being LINE of G st a <> b holds

( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) )

let a, b be POINT of G; :: thesis: for L being LINE of G st a <> b holds

( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) )

let L be LINE of G; :: thesis: ( a <> b implies ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) )

assume A1: a <> b ; :: thesis: ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) )

then {a,b} on a * b by Def8;

hence ( a on a * b & b on a * b & a * b = b * a ) by A1, Def8, INCSP_1:1; :: thesis: ( a on L & b on L implies L = a * b )

assume ( a on L & b on L ) ; :: thesis: L = a * b

then {a,b} on L by INCSP_1:1;

hence L = a * b by A1, Def8; :: thesis: verum

for L being LINE of G st a <> b holds

( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) )

let a, b be POINT of G; :: thesis: for L being LINE of G st a <> b holds

( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) )

let L be LINE of G; :: thesis: ( a <> b implies ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) )

assume A1: a <> b ; :: thesis: ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) )

then {a,b} on a * b by Def8;

hence ( a on a * b & b on a * b & a * b = b * a ) by A1, Def8, INCSP_1:1; :: thesis: ( a on L & b on L implies L = a * b )

assume ( a on L & b on L ) ; :: thesis: L = a * b

then {a,b} on L by INCSP_1:1;

hence L = a * b by A1, Def8; :: thesis: verum