let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, d being POINT of S holds
( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )
let a, b, c, d be POINT of S; ( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )
A1:
( a,b <= c,d implies ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )
proof
assume
a,
b <= c,
d
;
ex x being POINT of S st
( between a,b,x & a,x equiv c,d )
then consider y being
POINT of
S such that A2:
(
between c,
y,
d &
a,
b equiv c,
y )
;
Collinear c,
y,
d
by A2;
then consider x being
POINT of
S such that A3:
c,
y,
d cong a,
b,
x
by A2, Satz2p2, Satz4p14;
a,
x equiv c,
d
by A3, Satz2p2;
hence
ex
x being
POINT of
S st
(
between a,
b,
x &
a,
x equiv c,
d )
by A2, A3, Satz4p6;
verum
end;
( ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) implies a,b <= c,d )
proof
assume
ex
x being
POINT of
S st
(
between a,
b,
x &
a,
x equiv c,
d )
;
a,b <= c,d
then consider x being
POINT of
S such that A4:
(
between a,
b,
x &
a,
x equiv c,
d )
;
A5:
Collinear x,
a,
b
by A4;
x,
a equiv c,
d
by A4, Satz2p4;
then consider y being
POINT of
S such that A6:
x,
a,
b cong d,
c,
y
by A5, Satz2p5, Satz4p14;
a,
b,
x cong c,
y,
d
hence
a,
b <= c,
d
by A4, Satz4p6;
verum
end;
hence
( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )
by A1; verum