let S be non empty TarskiGeometryStruct ; :: thesis:

hereby :: thesis:

assume A1: S is satisfying_Continuity_Axiom ; :: thesis:

now :: thesis:

let X, Y be set ; :: thesis:
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:
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:
assume ( x in X9 & y in Y9 ) ; :: thesis:
then ( x in X & y in Y ) by XBOOLE_0:def 4;
hence between a,x,y by A3; :: thesis:

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:
assume ( x in X & y in Y ) ; :: thesis:
then ( x in X9 & y in Y9 ) by XBOOLE_0:def 4;
hence between x,b,y by A4; :: thesis:

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:

end;

hence S is (Co) ; :: thesis:

end;

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