let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for p, q, r being POINT of S st p <> q & p <> r & between q,p,r holds
Line (p,q) = ((halfline (p,q)) \/ {p}) \/ (halfline (p,r))
let p, q, r be POINT of S; :: thesis: ( p <> q & p <> r & between q,p,r implies Line (p,q) = ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) )
assume that
A1A: p <> q and
A1B: p <> r and
A1C: between q,p,r ; :: thesis: Line (p,q) = ((halfline (p,q)) \/ {p}) \/ (halfline (p,r))
thus Line (p,q) c= ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) :: according to XBOOLE_0:def 10 :: thesis: ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) c= Line (p,q)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Line (p,q) or t in ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) )
assume t in Line (p,q) ; :: thesis: t in ((halfline (p,q)) \/ {p}) \/ (halfline (p,r))
then consider x being Element of S such that
A2: ( t = x & Collinear p,q,x ) ;
A3: ( between q,x,p & p <> x implies x in halfline (p,q) )
proof
assume ( between q,x,p & p <> x ) ; :: thesis: x in halfline (p,q)
then p out x,q by A1A, Satz3p2;
hence x in halfline (p,q) ; :: thesis: verum
end;
A4: ( between x,p,q & x = q implies p = x ) by GTARSKI1:def 10;
A5: ( between x,p,q & p <> x & x <> q implies x in halfline (p,r) )
proof
assume A6: ( between x,p,q & p <> x & x <> q ) ; :: thesis: x in halfline (p,r)
then ( between q,p,r & between q,p,x ) by A1C, Satz3p2;
then p out x,r by A1A, A1B, A6, Satz5p2;
hence x in halfline (p,r) ; :: thesis: verum
end;
( between p,q,x & p <> x implies x in halfline (p,q) )
proof
assume ( between p,q,x & p <> x ) ; :: thesis: x in halfline (p,q)
then p out x,q by A1A;
hence x in halfline (p,q) ; :: thesis: verum
end;
then ( x in halfline (p,q) or x in {p} or x in halfline (p,r) ) by A2, A3, A5, A4, TARSKI:def 1;
then ( x in (halfline (p,q)) \/ {p} or x in halfline (p,r) ) by XBOOLE_0:def 3;
hence t in ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
thus ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) c= Line (p,q) :: thesis: verum
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) or t in Line (p,q) )
assume t in ((halfline (p,q)) \/ {p}) \/ (halfline (p,r)) ; :: thesis: t in Line (p,q)
then ( t in (halfline (p,q)) \/ {p} or t in halfline (p,r) ) by XBOOLE_0:def 3;
then ( t in halfline (p,q) or t in {p} or t in halfline (p,r) ) by XBOOLE_0:def 3;
per cases then ( t in halfline (p,q) or t = p or t in halfline (p,r) ) by TARSKI:def 1;
suppose t in halfline (p,q) ; :: thesis: t in Line (p,q)
then consider x being POINT of S such that
A7: ( t = x & p out x,q ) ;
Collinear p,q,x by A7, Satz3p2;
hence t in Line (p,q) by A7; :: thesis: verum
end;
suppose A8: t = p ; :: thesis: t in Line (p,q)
then reconsider x = t as POINT of S ;
Collinear p,q,p by Satz3p1;
hence t in Line (p,q) by A8; :: thesis: verum
end;
suppose t in halfline (p,r) ; :: thesis: t in Line (p,q)
then consider x being POINT of S such that
A9: ( t = x & p out x,r ) ;
A10: ( not between p,x,r or between p,q,x or between q,x,p or between x,p,q )
proof
assume between p,x,r ; :: thesis: ( between p,q,x or between q,x,p or between x,p,q )
then between q,p,x by A1C, Satz3p5p1;
hence ( between p,q,x or between q,x,p or between x,p,q ) by Satz3p2; :: thesis: verum
end;
( not between p,r,x or between p,q,x or between q,x,p or between x,p,q )
proof
assume between p,r,x ; :: thesis: ( between p,q,x or between q,x,p or between x,p,q )
then between q,p,x by A1B, A1C, Satz3p7p2;
hence ( between p,q,x or between q,x,p or between x,p,q ) by Satz3p2; :: thesis: verum
end;
then Collinear p,q,x by A9, A10;
hence t in Line (p,q) by A9; :: thesis: verum
end;
end;
end;