let M be non empty Reflexive triangle MetrStruct ; :: thesis: for a being Point of M
for X being non empty set st WellSpace (a,X) is complete holds
M is complete
let a be Point of M; :: thesis: for X being non empty set st WellSpace (a,X) is complete holds
M is complete
let X be non empty set ; :: thesis: ( WellSpace (a,X) is complete implies M is complete )
consider x0 being set such that
A1: x0 in X by XBOOLE_0:def 1;
set W = WellSpace (a,X);
assume A2: WellSpace (a,X) is complete ; :: thesis: M is complete
let S be sequence of M; :: according to TBSP_1:def 5 :: thesis: ( not S is Cauchy or S is convergent )
assume A3: S is Cauchy ; :: thesis: S is convergent
defpred S₁[ set , set ] means ( ( S . $1 <> a implies $2 = [x0,(S . $1)] ) & ( S . $1 = a implies $2 = [X,(S . $1)] ) );
A4: for x being set st x in NAT holds
ex y being set st
( y in the carrier of (WellSpace (a,X)) & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in the carrier of (WellSpace (a,X)) & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in the carrier of (WellSpace (a,X)) & S₁[x,y] )
then reconsider i = x as Element of NAT ;

per cases ( S . i <> a or S . x = a ) ;

suppose A5: S . i <> a ; :: thesis: ex y being set st
( y in the carrier of (WellSpace (a,X)) & S₁[x,y] )

take [x0,(S . i)] ; :: thesis: ( [x0,(S . i)] in the carrier of (WellSpace (a,X)) & S₁[x,[x0,(S . i)]] )
thus ( [x0,(S . i)] in the carrier of (WellSpace (a,X)) & S₁[x,[x0,(S . i)]] ) by A1, A5, Th38; :: thesis: verum

end;

suppose A6: S . x = a ; :: thesis: ex y being set st
( y in the carrier of (WellSpace (a,X)) & S₁[x,y] )

take [X,a] ; :: thesis: ( [X,a] in the carrier of (WellSpace (a,X)) & S₁[x,[X,a]] )
thus ( [X,a] in the carrier of (WellSpace (a,X)) & S₁[x,[X,a]] ) by A6, Th38; :: thesis: verum

end;

end;

end;

consider S9 being sequence of (WellSpace (a,X)) such that
A7: for x being set st x in NAT holds
S₁[x,S9 . x] from FUNCT_2:sch 1(A4);
S9 is Cauchy

proof

let r be Real; :: according to TBSP_1:def 4 :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S9 . b₂),(S9 . b₃)) ) )
assume r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S9 . b₂),(S9 . b₃)) )
then consider p being Element of NAT such that
A8: for n, m being Element of NAT st p <= n & p <= m holds
dist ((S . n),(S . m)) < r by A3, TBSP_1:def 4;
take p ; :: thesis: for b₁, b₂ being Element of NAT holds
( not p <= b₁ or not p <= b₂ or not r <= dist ((S9 . b₁),(S9 . b₂)) )
let n, m be Element of NAT ; :: thesis: ( not p <= n or not p <= m or not r <= dist ((S9 . n),(S9 . m)) )
assume that
A9: p <= n and
A10: p <= m ; :: thesis: not r <= dist ((S9 . n),(S9 . m))

per cases ( ( S . n = a & S . m = a ) or ( S . n <> a & S . m = a ) or ( S . n = a & S . m <> a ) or ( S . n <> a & S . m <> a ) ) ;

suppose A11: ( S . n = a & S . m = a ) ; :: thesis: not r <= dist ((S9 . n),(S9 . m))

then A12: [X,(S . m)] = S9 . m by A7;
[X,(S . n)] = S9 . n by A7, A11;
then dist ((S9 . n),(S9 . m)) = dist ((S . n),(S . m)) by A12, Def10;
hence not r <= dist ((S9 . n),(S9 . m)) by A8, A9, A10; :: thesis: verum

end;

suppose A13: ( S . n <> a & S . m = a ) ; :: thesis: not r <= dist ((S9 . n),(S9 . m))

then A14: [X,(S . m)] = S9 . m by A7;
A15: dist ((S . m),(S . m)) = 0 by METRIC_1:1;
A16: X <> x0 by A1;
[x0,(S . n)] = S9 . n by A7, A13;
then dist ((S9 . n),(S9 . m)) = (dist ((S . n),(S . m))) + (dist ((S . m),(S . m))) by A13, A14, A16, Def10;
hence not r <= dist ((S9 . n),(S9 . m)) by A8, A9, A10, A15; :: thesis: verum

end;

suppose A17: ( S . n = a & S . m <> a ) ; :: thesis: not r <= dist ((S9 . n),(S9 . m))

then A18: [x0,(S . m)] = S9 . m by A7;
A19: dist ((S . n),(S . n)) = 0 by METRIC_1:1;
A20: X <> x0 by A1;
[X,(S . n)] = S9 . n by A7, A17;
then dist ((S9 . n),(S9 . m)) = (dist ((S . n),(S . n))) + (dist ((S . n),(S . m))) by A17, A18, A20, Def10;
hence not r <= dist ((S9 . n),(S9 . m)) by A8, A9, A10, A19; :: thesis: verum

end;

suppose A21: ( S . n <> a & S . m <> a ) ; :: thesis: not r <= dist ((S9 . n),(S9 . m))

then A22: [x0,(S . m)] = S9 . m by A7;
[x0,(S . n)] = S9 . n by A7, A21;
then dist ((S9 . n),(S9 . m)) = dist ((S . n),(S . m)) by A22, Def10;
hence not r <= dist ((S9 . n),(S9 . m)) by A8, A9, A10; :: thesis: verum

end;

end;

end;

then S9 is convergent by A2, TBSP_1:def 5;
then consider L being Element of (WellSpace (a,X)) such that
A23: for r being Real st r > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
dist ((S9 . m),L) < r by TBSP_1:def 2;
consider L1 being set , L2 being Point of M such that
A24: L = [L1,L2] and
( ( L1 in X & L2 <> a ) or ( L1 = X & L2 = a ) ) by Th38;
take L2 ; :: according to TBSP_1:def 2 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= dist ((S . b₃),L2) ) )
let r be Real; :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not r <= dist ((S . b₂),L2) ) )
assume r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not r <= dist ((S . b₂),L2) )
then consider n being Element of NAT such that
A25: for m being Element of NAT st n <= m holds
dist ((S9 . m),L) < r by A23;
take n ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not r <= dist ((S . b₁),L2) )
let m be Element of NAT ; :: thesis: ( not n <= m or not r <= dist ((S . m),L2) )
assume A26: n <= m ; :: thesis: not r <= dist ((S . m),L2)

per cases ( ( S . m = a & L1 = X ) or ( S . m = a & L1 <> X ) or ( S . m <> a & L1 = x0 ) or ( S . m <> a & L1 <> x0 ) ) ;

suppose A27: ( S . m = a & L1 = X ) ; :: thesis: not r <= dist ((S . m),L2)

then S9 . m = [X,a] by A7;
then dist ((S9 . m),L) = dist ((S . m),L2) by A24, A27, Def10;
hence not r <= dist ((S . m),L2) by A25, A26; :: thesis: verum

end;

suppose A28: ( S . m = a & L1 <> X ) ; :: thesis: not r <= dist ((S . m),L2)

then S9 . m = [X,a] by A7;
then A29: dist ((S9 . m),L) = (dist ((S . m),(S . m))) + (dist ((S . m),L2)) by A24, A28, Def10;
dist ((S . m),(S . m)) = 0 by METRIC_1:1;
hence not r <= dist ((S . m),L2) by A25, A26, A29; :: thesis: verum

end;

suppose A30: ( S . m <> a & L1 = x0 ) ; :: thesis: not r <= dist ((S . m),L2)

then S9 . m = [x0,(S . m)] by A7;
then dist ((S9 . m),L) = dist ((S . m),L2) by A24, A30, Def10;
hence not r <= dist ((S . m),L2) by A25, A26; :: thesis: verum

end;

suppose A31: ( S . m <> a & L1 <> x0 ) ; :: thesis: not r <= dist ((S . m),L2)

then S9 . m = [x0,(S . m)] by A7;
then A32: dist ((S9 . m),L) = (dist ((S . m),a)) + (dist (a,L2)) by A24, A31, Def10;
A33: (dist ((S . m),a)) + (dist (a,L2)) >= dist ((S . m),L2) by METRIC_1:4;
dist ((S9 . m),L) < r by A25, A26;
hence not r <= dist ((S . m),L2) by A32, A33, XXREAL_0:2; :: thesis: verum

end;

end;