let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for p, q, r, s being POINT of S st p,q out s,r & p,r out s,q holds
between q, Line (p,s),r
let p, q, r, s be POINT of S; :: thesis: ( p,q out s,r & p,r out s,q implies between q, Line (p,s),r )
assume that
A1: p,q out s,r and
A2: p,r out s,q ; :: thesis: between q, Line (p,s),r
set A = Line (p,q);
set A9 = Line (p,r);
set A99 = Line (p,s);
Line (p,q) out s,r by A1;
then A3: ex x being POINT of S st
( between s, Line (p,q),x & between r, Line (p,q),x ) ;
Line (p,r) out s,q by A2;
then A4: ex x being POINT of S st
( between s, Line (p,r),x & between q, Line (p,r),x ) ;
per cases ( Line (p,q) = Line (p,r) or Line (p,q) <> Line (p,r) ) ;
suppose Line (p,q) = Line (p,r) ; :: thesis: between q, Line (p,s),r
hence between q, Line (p,s),r by A3, GTARSKI3:83; :: thesis: verum
end;
suppose A5: Line (p,q) <> Line (p,r) ; :: thesis: between q, Line (p,s),r
A6: ( Line (p,q) is_line & Line (p,r) is_line & Line (p,q) <> Line (p,r) & p in Line (p,r) & p in Line (p,q) ) by A1, A2, A5, GTARSKI3:83;
consider r9 being POINT of S such that
A7: between r,p,r9 and
A8: p <> r9 by GTARSKI3:36;
Collinear r,p,r9 by A7;
then A9: r9 in { x where x is POINT of S : Collinear r,p,x } ;
A10: not r9 in Line (p,q)
proof
assume r9 in Line (p,q) ; :: thesis: contradiction
then ( Line (p,q) is_line & Line (p,r) is_line & Line (p,q) <> Line (p,r) & p in Line (p,q) & r9 in Line (p,q) & p in Line (p,r) & r9 in Line (p,r) ) by A6, A9, GTARSKI3:def 10;
hence contradiction by A8, GTARSKI3:89; :: thesis: verum
end;
( Line (p,q) out r,s & between r, Line (p,q),r9 ) by A3, A7, A10, GTARSKI3:83;
then between s, Line (p,q),r9 by Th14;
then consider t being POINT of S such that
A11: t in Line (p,q) and
A12: between r9,t,s by GTARSKI3:14;
A13: not r9 in Line (p,s)
proof
assume r9 in Line (p,s) ; :: thesis: contradiction
then ( Line (p,s) is_line & Line (p,r) is_line & r9 in Line (p,s) & r9 in Line (p,r) & Line (p,r) <> Line (p,s) & p in Line (p,s) & p in Line (p,r) ) by A6, A9, A4, GTARSKI3:def 10, GTARSKI3:83;
hence contradiction by A8, GTARSKI3:89; :: thesis: verum
end;
A14: Line (p,r) <> Line (p,s)
proof
assume A15: Line (p,r) = Line (p,s) ; :: thesis: contradiction
Collinear p,r,r9 by A7, GTARSKI4:7;
hence contradiction by A13, A15; :: thesis: verum
end;
A16: Collinear t,s,r9 by A12;
A17: not t in Line (p,r)
proof
assume A18: t in Line (p,r) ; :: thesis: contradiction
A19: r9 in Line (p,r) by A9, GTARSKI3:def 10;
end;
now :: thesis: ( Line (p,s) is_line & p in Line (p,s) & Collinear t,q,p & p out t,q & not t in Line (p,s) )
thus Line (p,s) is_line by A3, A6; :: thesis: ( p in Line (p,s) & Collinear t,q,p & p out t,q & not t in Line (p,s) )
thus p in Line (p,s) by GTARSKI3:83; :: thesis: ( Collinear t,q,p & p out t,q & not t in Line (p,s) )
( Line (p,q) is_line & t in Line (p,q) & q in Line (p,q) & p in Line (p,q) ) by A1, A11, GTARSKI3:83;
hence Collinear t,q,p by GTARSKI3:90; :: thesis: ( p out t,q & not t in Line (p,s) )
W1: Line (p,r) is_line by A2;
W2: r9 in Line (p,r) by A9, GTARSKI3:def 10;
W3: Collinear t,s,r9 by A12;
W4: r9 out t,s by A11, A10, A12, GTARSKI1:def 10;
( Line (p,r) out t,s & Line (p,r) out s,q ) by A17, W1, W2, W3, W4, A2, Th29;
then G1: Line (p,r) out t,q by Th19;
G2: ( Line (p,r) is_line & p in Line (p,r) & Line (p,q) is_line & t in Line (p,q) & q in Line (p,q) & p in Line (p,q) ) by A1, A2, A11, GTARSKI3:83;
then Collinear t,q,p by GTARSKI3:90;
hence p out t,q by G1, G2, Th29; :: thesis: not t in Line (p,s)
thus not t in Line (p,s) :: thesis: verum
proof
assume t in Line (p,s) ; :: thesis: contradiction
then ex x being POINT of S st
( x = t & Collinear p,s,x ) ;
then Collinear p,t,s by GTARSKI3:45;
then A21: s in Line (p,t) ;
( p in Line (p,q) & t in Line (p,q) & p <> t & Line (p,q) is_line ) by A1, A11, A17, GTARSKI3:83;
hence contradiction by A21, A3, GTARSKI3:87; :: thesis: verum
end;
end;
then G1: Line (p,s) out t,q by Th29;
H1: Line (p,s) is_line by A3, A6;
H3: not r in Line (p,s)
proof
assume r in Line (p,s) ; :: thesis: contradiction
then A22: ( p in Line (p,r) & p in Line (p,s) & r in Line (p,s) & r in Line (p,r) ) by GTARSKI3:83;
( Line (p,r) is_line & Line (p,s) is_line & Line (p,r) <> Line (p,s) ) by A3, A6, A14;
then p = r by A22, GTARSKI3:89;
hence contradiction by A3, GTARSKI3:83; :: thesis: verum
end;
( p in Line (p,s) & between r9,p,r ) by A7, GTARSKI3:14, GTARSKI3:83;
then T1: between r9, Line (p,s),r by H1, A13, H3;
s out r9,t by A3, A11, A12, GTARSKI3:14, GTARSKI1:def 10;
then between t, Line (p,s),r by T1, GTARSKI3:83, Th12;
hence between q, Line (p,s),r by G1, Th14; :: thesis: verum
end;
end;