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