let CLSP be CollSp; :: thesis: for p, q being Element of CLSP holds Line (p,q) = Line (q,p)
let p, q be Element of CLSP; :: thesis: Line (p,q) = Line (q,p)
A1: Line (p,q) c= Line (q,p)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (p,q) or x in Line (q,p) )
assume x in Line (p,q) ; :: thesis: x in Line (q,p)
then x in { y where y is Element of CLSP : p,q,y are_collinear } by COLLSP:def 5;
then consider y being Element of CLSP such that
A2: y = x and
A3: p,q,y are_collinear ;
q,p,y are_collinear by A3, COLLSP:4;
then y in { y where y is Element of CLSP : q,p,y are_collinear } ;
hence x in Line (q,p) by A2, COLLSP:def 5; :: thesis: verum

end;

Line (q,p) c= Line (p,q)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (q,p) or x in Line (p,q) )
assume x in Line (q,p) ; :: thesis: x in Line (p,q)
then x in { y where y is Element of CLSP : q,p,y are_collinear } by COLLSP:def 5;
then consider y being Element of CLSP such that
A4: y = x and
A5: q,p,y are_collinear ;
p,q,y are_collinear by A5, COLLSP:4;
then y in { y where y is Element of CLSP : p,q,y are_collinear } ;
hence x in Line (p,q) by A4, COLLSP:def 5; :: thesis: verum

end;

hence Line (p,q) = Line (q,p) by A1; :: thesis: verum