let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, x being POINT of S st a <> b & a <> x & x on_line a,b & c on_line a,b holds
c on_line a,x
let a, b, c, x be POINT of S; ( a <> b & a <> x & x on_line a,b & c on_line a,b implies c on_line a,x )
assume that
H1:
a <> b
and
H2:
a <> x
; ( not x on_line a,b or not c on_line a,b or c on_line a,x )
assume
x on_line a,b
; ( not c on_line a,b or c on_line a,x )
then X1:
( between a,b,x or between a,x,b or between x,a,b )
by Bsymmetry;
assume H4:
c on_line a,b
; c on_line a,x
( between a,x,c or between a,c,x or between x,a,c )
proof
consider m being
POINT of
S such that X5:
(
between b,
a,
m &
a,
m equiv a,
b )
by A4;
X6:
a <> m
by H1, X5, EquivSymmetric, A3;
per cases
( ( between a,b,x & between a,b,c ) or ( between a,b,x & between a,c,b ) or ( between a,b,x & between c,a,b ) or ( between a,x,b & between a,b,c ) or ( between a,x,b & between a,c,b ) or ( between a,x,b & between c,a,b ) or ( between x,a,b & between a,b,c ) or ( between x,a,b & between a,c,b ) or ( between x,a,b & between c,a,b ) )
by X1, Bsymmetry, H4;
suppose X3:
(
between a,
b,
x &
between a,
b,
c )
;
( between a,x,c or between a,c,x or between x,a,c )then
(
between b,
x,
c or
between b,
c,
x )
by H1, Gupta;
then
(
a,
b,
x,
c are_ordered or
a,
b,
c,
x are_ordered )
by X3, BTransitivityOrdered;
hence
(
between a,
x,
c or
between a,
c,
x or
between x,
a,
c )
;
verum end; suppose
(
between a,
b,
x &
between a,
c,
b )
;
( between a,x,c or between a,c,x or between x,a,c )end; suppose
(
between a,
b,
x &
between c,
a,
b )
;
( between a,x,c or between a,c,x or between x,a,c )then
c,
a,
b,
x are_ordered
by H1, BTransitivityOrdered;
hence
(
between a,
x,
c or
between a,
c,
x or
between x,
a,
c )
by Bsymmetry;
verum end; suppose
(
between a,
x,
b &
between a,
b,
c )
;
( between a,x,c or between a,c,x or between x,a,c )end; suppose X4:
(
between a,
x,
b &
between a,
c,
b )
;
( between a,x,c or between a,c,x or between x,a,c )
between m,
a,
b
by X5, Bsymmetry;
then
(
between m,
a,
c &
between m,
a,
x )
by X4, B124and234then123;
hence
(
between a,
x,
c or
between a,
c,
x or
between x,
a,
c )
by X6, Gupta;
verum end; suppose
(
between a,
x,
b &
between c,
a,
b )
;
( between a,x,c or between a,c,x or between x,a,c )end; suppose
(
between x,
a,
b &
between a,
b,
c )
;
( between a,x,c or between a,c,x or between x,a,c )then
x,
a,
b,
c are_ordered
by H1, BTransitivityOrdered;
hence
(
between a,
x,
c or
between a,
c,
x or
between x,
a,
c )
;
verum end; suppose
(
between x,
a,
b &
between a,
c,
b )
;
( between a,x,c or between a,c,x or between x,a,c )end; suppose
(
between x,
a,
b &
between c,
a,
b )
;
( between a,x,c or between a,c,x or between x,a,c )then
(
between b,
a,
x &
between b,
a,
c )
by Bsymmetry;
hence
(
between a,
x,
c or
between a,
c,
x or
between x,
a,
c )
by H1, Gupta;
verum end; end;
end;
hence
c on_line a,x
by H2, Bsymmetry; verum