let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for p, q, s being POINT of S st p <> q & s <> p & s in Line (p,q) holds
Line (p,q) = Line (p,s)
let p, q, s be POINT of S; ( p <> q & s <> p & s in Line (p,q) implies Line (p,q) = Line (p,s) )
assume that
A1A:
p <> q
and
A1B:
s <> p
and
A1C:
s in Line (p,q)
; Line (p,q) = Line (p,s)
consider x being POINT of S such that
A2:
( s = x & Collinear p,q,x )
by A1C;
thus
Line (p,q) c= Line (p,s)
XBOOLE_0:def 10 Line (p,s) c= Line (p,q)proof
let t be
object ;
TARSKI:def 3 ( not t in Line (p,q) or t in Line (p,s) )
assume
t in Line (
p,
q)
;
t in Line (p,s)
then consider y being
POINT of
S such that A3:
(
t = y &
Collinear p,
q,
y )
;
A4:
( not
between p,
q,
y or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume A5:
between p,
q,
y
;
( between p,s,y or between s,y,p or between y,p,s )
A6:
( not
between p,
q,
s or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between p,
q,
s
;
( between p,s,y or between s,y,p or between y,p,s )
then
(
between p,
y,
s or
between p,
s,
y )
by A1A, A5, Satz5p1;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by Satz3p2;
verum
end;
A7:
( not
between q,
s,
p or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between q,
s,
p
;
( between p,s,y or between s,y,p or between y,p,s )
then
between p,
s,
q
by Satz3p2;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by A5, Satz3p6p2;
verum
end;
( not
between s,
p,
q or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between s,
p,
q
;
( between p,s,y or between s,y,p or between y,p,s )
then
between s,
p,
y
by A1A, A5, Satz3p7p2;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by Satz3p2;
verum
end;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by A2, A6, A7;
verum
end;
A8:
( not
between q,
y,
p or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between q,
y,
p
;
( between p,s,y or between s,y,p or between y,p,s )
then A9:
between p,
y,
q
by Satz3p2;
A10:
( not
between p,
q,
s or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between p,
q,
s
;
( between p,s,y or between s,y,p or between y,p,s )
then
between p,
y,
s
by A9, Satz3p6p2;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by Satz3p2;
verum
end;
A11:
( not
between q,
s,
p or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between q,
s,
p
;
( between p,s,y or between s,y,p or between y,p,s )
then
between p,
s,
q
by Satz3p2;
then
(
between p,
s,
y or
between p,
y,
s )
by A9, Satz5p3;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by Satz3p2;
verum
end;
( not
between s,
p,
q or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between s,
p,
q
;
( between p,s,y or between s,y,p or between y,p,s )
then
between s,
p,
y
by A9, Satz3p5p1;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by Satz3p2;
verum
end;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by A2, A10, A11;
verum
end;
( not
between y,
p,
q or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume A12:
between y,
p,
q
;
( between p,s,y or between s,y,p or between y,p,s )
A13:
( not
between q,
s,
p or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume A14:
between q,
s,
p
;
( between p,s,y or between s,y,p or between y,p,s )
between q,
p,
y
by A12, Satz3p2;
then
between s,
p,
y
by A14, Satz3p6p1;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by Satz3p2;
verum
end;
( not
between s,
p,
q or
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
proof
assume
between s,
p,
q
;
( between p,s,y or between s,y,p or between y,p,s )
then
(
between q,
p,
s &
between q,
p,
y )
by A12, Satz3p2;
then
(
between p,
s,
y or
between p,
y,
s )
by A1A, Satz5p2;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by Satz3p2;
verum
end;
hence
(
between p,
s,
y or
between s,
y,
p or
between y,
p,
s )
by A2, A12, A1A, Satz3p7p2, A13;
verum
end;
then
Collinear p,
s,
y
by A4, A8, A3;
hence
t in Line (
p,
s)
by A3;
verum
end;
thus
Line (p,s) c= Line (p,q)
verumproof
let t be
object ;
TARSKI:def 3 ( not t in Line (p,s) or t in Line (p,q) )
assume
t in Line (
p,
s)
;
t in Line (p,q)
then consider y being
POINT of
S such that A15:
(
t = y &
Collinear p,
s,
y )
;
A16:
( not
between p,
s,
y or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume A17:
between p,
s,
y
;
( between p,q,y or between q,y,p or between y,p,q )
A18:
( not
between q,
s,
p or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume
between q,
s,
p
;
( between p,q,y or between q,y,p or between y,p,q )
then
between p,
s,
q
by Satz3p2;
then
(
between p,
q,
y or
between p,
y,
q )
by A17, A1B, Satz5p1;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by Satz3p2;
verum
end;
( not
between s,
p,
q or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume
between s,
p,
q
;
( between p,q,y or between q,y,p or between y,p,q )
then
between q,
p,
s
by Satz3p2;
then
between q,
p,
y
by A1B, A17, Satz3p7p2;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by Satz3p2;
verum
end;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by A17, Satz3p6p2, A18, A2;
verum
end;
A19:
( not
between s,
y,
p or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume A20:
between s,
y,
p
;
( between p,q,y or between q,y,p or between y,p,q )
A21:
( not
between p,
q,
s or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume A22:
between p,
q,
s
;
( between p,q,y or between q,y,p or between y,p,q )
between p,
y,
s
by A20, Satz3p2;
then
(
between p,
q,
y or
between p,
y,
q )
by A22, Satz5p3;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by Satz3p2;
verum
end;
A23:
( not
between q,
s,
p or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume
between q,
s,
p
;
( between p,q,y or between q,y,p or between y,p,q )
then A25:
between p,
s,
q
by Satz3p2;
between p,
y,
s
by A20, Satz3p2;
then
between p,
y,
q
by A25, Satz3p6p2;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by Satz3p2;
verum
end;
( not
between s,
p,
q or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume
between s,
p,
q
;
( between p,q,y or between q,y,p or between y,p,q )
then A26:
between q,
p,
s
by Satz3p2;
between p,
y,
s
by A20, Satz3p2;
then
between q,
p,
y
by A26, Satz3p5p1;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by Satz3p2;
verum
end;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by A21, A23, A2;
verum
end;
( not
between y,
p,
s or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume A27:
between y,
p,
s
;
( between p,q,y or between q,y,p or between y,p,q )
A28:
( not
between q,
s,
p or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume
between q,
s,
p
;
( between p,q,y or between q,y,p or between y,p,q )
then
between p,
s,
q
by Satz3p2;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by A27, A1B, Satz3p7p2;
verum
end;
( not
between s,
p,
q or
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
proof
assume A29:
between s,
p,
q
;
( between p,q,y or between q,y,p or between y,p,q )
between s,
p,
y
by A27, Satz3p2;
then
(
between p,
q,
y or
between p,
y,
q )
by Satz5p2, A29, A1B;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by Satz3p2;
verum
end;
hence
(
between p,
q,
y or
between q,
y,
p or
between y,
p,
q )
by A27, Satz3p5p1, A28, A2;
verum
end;
then
Collinear p,
q,
y
by A15, A16, A19;
hence
t in Line (
p,
q)
by A15;
verum
end;