let CLSP be proper CollSp; :: thesis: for P, Q being LINE of CLSP holds
( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )
let P, Q be LINE of CLSP; :: thesis: ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} )
A1: ( ex a being set st {a} = P /\ Q implies ex p being Point of CLSP st P /\ Q = {p} )

proof

given a being set such that A2: {a} = P /\ Q ; :: thesis: ex p being Point of CLSP st P /\ Q = {p}
a in P /\ Q by A2, TARSKI:def 1;
then a in P by XBOOLE_0:def 4;
then reconsider p = a as Point of CLSP by Lm9;
P /\ Q = {p} by A2;
hence ex p being Point of CLSP st P /\ Q = {p} ; :: thesis: verum

end;

A3: ( ex a, b being set st
( a <> b & a in P /\ Q & b in P /\ Q ) implies P = Q )

proof

given a, b being set such that A4: a <> b and
A5: ( a in P /\ Q & b in P /\ Q ) ; :: thesis: P = Q
( a in P & b in P ) by A5, XBOOLE_0:def 4;
then reconsider p = a, q = b as Point of CLSP by Lm9;
A6: ( p in Q & q in Q ) by A5, XBOOLE_0:def 4;
( p in P & q in P ) by A5, XBOOLE_0:def 4;
hence P = Q by A4, A6, Th20; :: thesis: verum

end;

( P /\ Q = {} or ex a being set st
( {a} = P /\ Q or ex a, b being set st
( a <> b & a in P /\ Q & b in P /\ Q ) ) ) by Th1;
hence ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} ) by A1, A3, XBOOLE_0:def 7; :: thesis: verum