let S be non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; for p, q being POINT of S holds
( p in Line (p,q) & q in Line (p,q) & Line (p,q) = Line (q,p) )
let p, q be POINT of S; ( p in Line (p,q) & q in Line (p,q) & Line (p,q) = Line (q,p) )
thus
p in Line (p,q)
( q in Line (p,q) & Line (p,q) = Line (q,p) )
Collinear p,q,q
by Satz3p1;
hence
q in Line (p,q)
; Line (p,q) = Line (q,p)
thus
Line (p,q) = Line (q,p)
verumproof
A2:
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 consider y being
POINT of
S such that A3:
y = x
and A4:
Collinear p,
q,
y
;
Collinear q,
p,
y
by A4, Satz3p2;
hence
x in Line (
q,
p)
by A3;
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 consider y being
POINT of
S such that A5:
y = x
and A6:
Collinear q,
p,
y
;
Collinear p,
q,
y
by A6, Satz3p2;
hence
x in Line (
p,
q)
by A5;
verum
end;
hence
Line (
p,
q)
= Line (
q,
p)
by A2;
verum
end;