let CLSP be proper CollSp; :: thesis: for P, Q being LINE of CLSP st P c= Q holds
P = Q
let P, Q be LINE of CLSP; :: thesis: ( P c= Q implies P = Q )
assume A1: P c= Q ; :: thesis: P = Q
Q c= P

proof

let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in Q or r in P )
consider p, q being Point of CLSP such that
p <> q and
A2: P = Line (p,q) by Def7;
assume A3: r in Q ; :: thesis: r in P
then reconsider r = r as Point of CLSP by Lm9;
( p in P & q in P ) by A2, Th10;
then p,q,r are_collinear by A1, A3, Th16;
hence r in P by A2; :: thesis: verum

end;

hence P = Q by A1, XBOOLE_0:def 10; :: thesis: verum