let S be non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( p in Line (p,q) & q in Line (p,q) & Line (p,q) = Line (q,p) )
thus p in Line (p,q) :: thesis: ( q in Line (p,q) & Line (p,q) = Line (q,p) )
proof
Collinear p,q,p by Satz3p1;
hence p in Line (p,q) ; :: thesis: verum
end;
Collinear p,q,q by Satz3p1;
hence q in Line (p,q) ; :: thesis: Line (p,q) = Line (q,p)
thus Line (p,q) = Line (q,p) :: thesis: verum
proof
A2: 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 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; :: 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 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; :: thesis: verum
end;
hence Line (p,q) = Line (q,p) by A2; :: thesis: verum
end;