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