let S be IncSpace; :: thesis: for A, B being POINT of S st A <> B holds

ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L )

let A, B be POINT of S; :: thesis: ( A <> B implies ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L ) )

assume A1: A <> B ; :: thesis: ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L )

consider L being LINE of S such that

A2: {A,B} on L by Def9;

take L ; :: thesis: for K being LINE of S holds

( {A,B} on K iff K = L )

thus for K being LINE of S holds

( {A,B} on K iff K = L ) by A1, A2, Def10; :: thesis: verum

ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L )

let A, B be POINT of S; :: thesis: ( A <> B implies ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L ) )

assume A1: A <> B ; :: thesis: ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L )

consider L being LINE of S such that

A2: {A,B} on L by Def9;

take L ; :: thesis: for K being LINE of S holds

( {A,B} on K iff K = L )

thus for K being LINE of S holds

( {A,B} on K iff K = L ) by A1, A2, Def10; :: thesis: verum