let S be non empty TarskiGeometryStruct ; :: thesis: ( S is satisfying_Continuity_Axiom iff S is (Co) )

hereby :: thesis: ( S is (Co) implies S is satisfying_Continuity_Axiom )

assume A1: S is satisfying_Continuity_Axiom ; :: thesis: S is (Co)

now :: thesis: for X, Y being set st ex a being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between a,x,y holds
ex b being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between x,b,y

let X, Y be set ; :: thesis: ( ex a being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between a,x,y implies ex b being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between x,b,y )
reconsider X9 = X /\ the carrier of S, Y9 = Y /\ the carrier of S as Subset of S by XBOOLE_1:17;
assume ex a being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between a,x,y ; :: thesis: ex b being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between x,b,y
then consider a being POINT of S such that
A3: for x, y being POINT of S st x in X & y in Y holds
between a,x,y ;
for x, y being POINT of S st x in X9 & y in Y9 holds
between a,x,y

proof

let x, y be POINT of S; :: thesis: ( x in X9 & y in Y9 implies between a,x,y )
assume ( x in X9 & y in Y9 ) ; :: thesis: between a,x,y
then ( x in X & y in Y ) by XBOOLE_0:def 4;
hence between a,x,y by A3; :: thesis: verum

end;

then consider b being POINT of S such that
A4: for x, y being POINT of S st x in X9 & y in Y9 holds
between x,b,y by A1;
for x, y being POINT of S st x in X & y in Y holds
between x,b,y

proof

let x, y be POINT of S; :: thesis: ( x in X & y in Y implies between x,b,y )
assume ( x in X & y in Y ) ; :: thesis: between x,b,y
then ( x in X9 & y in Y9 ) by XBOOLE_0:def 4;
hence between x,b,y by A4; :: thesis: verum

end;

hence ex b being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between x,b,y ; :: thesis: verum

end;

hence S is (Co) ; :: thesis: verum

end;

assume S is (Co) ; :: thesis: S is satisfying_Continuity_Axiom
hence S is satisfying_Continuity_Axiom ; :: thesis: verum