let CLSP be CollSp; for p, q being Element of CLSP holds Line (p,q) = Line (q,p)
let p, q be Element of CLSP; Line (p,q) = Line (q,p)
A1:
Line (p,q) c= Line (q,p)
proof
let x be
object ;
TARSKI:def 3 ( not x in Line (p,q) or x in Line (q,p) )
assume
x in Line (
p,
q)
;
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;
verum
end;
Line (q,p) c= Line (p,q)
proof
let x be
object ;
TARSKI:def 3 ( not x in Line (q,p) or x in Line (p,q) )
assume
x in Line (
q,
p)
;
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;
verum
end;
hence
Line (p,q) = Line (q,p)
by A1; verum