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 object 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₁[ object , object ] means ( ( S . $1 <> a implies $2 = [x0,(S . $1)] ) & ( S . $1 = a implies $2 = [X,(S . $1)] ) );
A4: for x being object st x in NAT holds
ex y being object st
( y in the carrier of (WellSpace (a,X)) & S₁[x,y] )

proof

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

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

suppose A5: S . i <> a ; :: thesis: ex y being object 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, Th37; :: thesis: verum

end;

suppose A6: S . x = a ; :: thesis: ex y being object 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, Th37; :: thesis: verum

end;

end;

end;

consider S9 being sequence of (WellSpace (a,X)) such that
A7: for x being object 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 set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S9 . b₂),(S9 . b₃)) ) )
assume r > 0 ; :: thesis: ex b₁ being set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S9 . b₂),(S9 . b₃)) )
then consider p being Nat such that
A8: for n, m being Nat st p <= n & p <= m holds
dist ((S . n),(S . m)) < r by A3;
take p ; :: thesis: for b₁, b₂ being set holds
( not p <= b₁ or not p <= b₂ or not r <= dist ((S9 . b₁),(S9 . b₂)) )
let n, m be 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))
A11: ( n in NAT & m in NAT ) by ORDINAL1:def 12;

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 A12: ( S . n = a & S . m = a ) ; :: thesis: not r <= dist ((S9 . n),(S9 . m))

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

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 A29: ( S . m = a & L1 = X ) ; :: thesis: not r <= dist ((S . m),L2)

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

end;

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

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

end;

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

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

end;

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

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

end;

end;