let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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) :: according to XBOOLE_0:def 10 :: thesis: Line (p,s) c= Line (p,q)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Line (p,q) or t in Line (p,s) )
assume t in Line (p,q) ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
hence ( between p,s,y or between s,y,p or between y,p,s ) by A2, A6, A7; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
hence ( between p,s,y or between s,y,p or between y,p,s ) by A2, A10, A11; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
hence ( between p,s,y or between s,y,p or between y,p,s ) by A2, A12, A1A, Satz3p7p2, A13; :: thesis: verum
end;
then Collinear p,s,y by A4, A8, A3;
hence t in Line (p,s) by A3; :: thesis: verum
end;
thus Line (p,s) c= Line (p,q) :: thesis: verum
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Line (p,s) or t in Line (p,q) )
assume t in Line (p,s) ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
hence ( between p,q,y or between q,y,p or between y,p,q ) by A17, Satz3p6p2, A18, A2; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
hence ( between p,q,y or between q,y,p or between y,p,q ) by A21, A23, A2; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
hence ( between p,q,y or between q,y,p or between y,p,q ) by A27, Satz3p5p1, A28, A2; :: thesis: verum
end;
then Collinear p,q,y by A15, A16, A19;
hence t in Line (p,q) by A15; :: thesis: verum
end;