:: PCOMPS_1 semantic presentation

begin


theorem Th1: :: PCOMPS_1:1
for PM being MetrStruct
for x being Element of PM
for r, p being real number st r <= p holds
Ball (x,r) c= Ball (x,p)
proof
let PM be MetrStruct ; ::_thesis: for x being Element of PM
for r, p being real number st r <= p holds
Ball (x,r) c= Ball (x,p)
let x be Element of PM; ::_thesis: for r, p being real number st r <= p holds
Ball (x,r) c= Ball (x,p)
let r, p be real number ; ::_thesis: ( r <= p implies Ball (x,r) c= Ball (x,p) )
assume A1: r <= p ; ::_thesis: Ball (x,r) c= Ball (x,p)
 for y being Element of PM st y in Ball (x,r) holds
y in Ball (x,p)
proof
let y be Element of PM; ::_thesis: ( y in Ball (x,r) implies y in Ball (x,p) )
assume A2: y in Ball (x,r) ; ::_thesis: y in Ball (x,p)
then  dist (x,y) < r by METRIC_1:11;
then A3: dist (x,y) < p by A1, XXREAL_0:2;
 not PM is empty by A2;
hence  y in Ball (x,p) by A3, METRIC_1:11; ::_thesis: verum
end;
hence  Ball (x,r) c= Ball (x,p) by SUBSET_1:2; ::_thesis: verum
end;


theorem Th2: :: PCOMPS_1:2
for T being TopSpace
for A being Subset of T holds
( Cl A <> {} iff A <> {} )
proof
let T be TopSpace; ::_thesis: for A being Subset of T holds
( Cl A <> {} iff A <> {} )
let A be Subset of T; ::_thesis: ( Cl A <> {} iff A <> {} )
 ( A <> {} implies Cl A <> {} )
proof
set x = the Element of A;
A1: A c= Cl A by PRE_TOPC:18;
assume A2: A <> {} ; ::_thesis: Cl A <> {}
 ex x being set st x in Cl A
proof
take  the Element of A ; ::_thesis: the Element of A in Cl A
thus  the Element of A in Cl A by A2, A1, TARSKI:def_3; ::_thesis: verum
end;
hence  Cl A <> {} ; ::_thesis: verum
end;
hence  ( Cl A <> {} iff A <> {} ) by PRE_TOPC:22; ::_thesis: verum
end;


theorem Th3: :: PCOMPS_1:3
for T being non empty TopSpace
for FX being Subset-Family of T st FX is Cover of T holds
for x being Point of T ex W being Subset of T st
( x in W & W in FX )
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is Cover of T holds
for x being Point of T ex W being Subset of T st
( x in W & W in FX )
let FX be Subset-Family of T; ::_thesis: ( FX is Cover of T implies for x being Point of T ex W being Subset of T st
( x in W & W in FX ) )
assume  FX is Cover of T ; ::_thesis: for x being Point of T ex W being Subset of T st
( x in W & W in FX )
then A1: union FX = [#] T by SETFAM_1:45;
thus  for x being Point of T ex W being Subset of T st
( x in W & W in FX ) ::_thesis: verum
proof
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W in FX )
thus  ex W being Subset of T st
( x in W & W in FX ) ::_thesis: verum
proof
consider W being set  such that
A2: x in W and
A3: W in FX by A1, TARSKI:def_4;
reconsider W = W as Subset of T by A3;
take  W ; ::_thesis: ( x in W & W in FX )
thus  ( x in W & W in FX ) by A2, A3; ::_thesis: verum
end;
end;
end;

theorem :: PCOMPS_1:4
for a being set holds the topology of (1TopSp a) = bool a ;

theorem :: PCOMPS_1:5
for a being set holds the carrier of (1TopSp a) = a ;

theorem :: PCOMPS_1:6
for a being set holds 1TopSp {a} is compact ;

theorem :: PCOMPS_1:7
for T being non empty TopSpace
for x being Point of T st T is T_2 holds
{x} is closed ;


definition
let T be TopStruct ;
let IT be Subset-Family of T;
attrIT is locally_finite  means :Def1: :: PCOMPS_1:def 1
 for x being Point of T ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in IT & V meets W )  }  is finite );
end;

:: deftheorem Def1 defines locally_finite PCOMPS_1:def_1_:_
 for T being TopStruct
for IT being Subset-Family of T holds
( IT is locally_finite iff for x being Point of T ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in IT & V meets W )  }  is finite ) );

theorem Th8: :: PCOMPS_1:8
for T being non empty TopSpace
for FX being Subset-Family of T
for W being Subset of T holds  {  V where V is Subset of T : ( V in FX & V meets W )  }  c= FX
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T
for W being Subset of T holds  {  V where V is Subset of T : ( V in FX & V meets W )  }  c= FX
let FX be Subset-Family of T; ::_thesis: for W being Subset of T holds  {  V where V is Subset of T : ( V in FX & V meets W )  }  c= FX
let W be Subset of T; ::_thesis:  {  V where V is Subset of T : ( V in FX & V meets W )  }  c= FX
now__::_thesis:_for_Y_being_set_st_Y_in__{__V_where_V_is_Subset_of_T_:_(_V_in_FX_&_V_meets_W_)__}__holds_
Y_in_FX
let Y be set ; ::_thesis: ( Y in  {  V where V is Subset of T : ( V in FX & V meets W )  }  implies Y in FX )
assume  Y in  {  V where V is Subset of T : ( V in FX & V meets W )  }  ; ::_thesis: Y in FX
then  ex V being Subset of T st
( Y = V & V in FX & V meets W ) ;
hence  Y in FX ; ::_thesis: verum
end;
hence   {  V where V is Subset of T : ( V in FX & V meets W )  }  c= FX by TARSKI:def_3; ::_thesis: verum
end;

theorem Th9: :: PCOMPS_1:9
for T being non empty TopSpace
for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite
proof
let T be non empty TopSpace; ::_thesis: for FX, GX being Subset-Family of T st FX c= GX & GX is locally_finite holds
FX is locally_finite
let FX, GX be Subset-Family of T; ::_thesis: ( FX c= GX & GX is locally_finite implies FX is locally_finite )
assume that
A1: FX c= GX and
A2: GX is locally_finite ; ::_thesis: FX is locally_finite
now__::_thesis:_for_x_being_Point_of_T_ex_W_being_Subset_of_T_st_
(_x_in_W_&_W_is_open_&__{__V_where_V_is_Subset_of_T_:_(_V_in_FX_&_V_meets_W_)__}__is_finite_)
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite )
thus  ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite ) ::_thesis: verum
proof
consider Y being Subset of T such that
A3: x in Y and
A4: Y is open and
A5:  {  X where X is Subset of T : ( X in GX & X meets Y )  }  is finite by A2, Def1;
take W = Y; ::_thesis: ( x in W & W is open &  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite )
thus  x in W by A3; ::_thesis: ( W is open &  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite )
thus  W is open by A4; ::_thesis:  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite
  {  V where V is Subset of T : ( V in FX & V meets W )  }  c=  {  X where X is Subset of T : ( X in GX & X meets Y )  }
proof
now__::_thesis:_for_Z_being_set_st_Z_in__{__V_where_V_is_Subset_of_T_:_(_V_in_FX_&_V_meets_W_)__}__holds_
Z_in__{__X_where_X_is_Subset_of_T_:_(_X_in_GX_&_X_meets_Y_)__}_
let Z be set ; ::_thesis: ( Z in  {  V where V is Subset of T : ( V in FX & V meets W )  }  implies Z in  {  X where X is Subset of T : ( X in GX & X meets Y )  }  )
assume A6: Z in  {  V where V is Subset of T : ( V in FX & V meets W )  }  ; ::_thesis: Z in  {  X where X is Subset of T : ( X in GX & X meets Y )  }
 ex X being Subset of T st
( Z = X & X in GX & X meets Y )
proof
consider V being Subset of T such that
A7: Z = V and
A8: V in FX and
A9: V meets W by A6;
take X = V; ::_thesis: ( Z = X & X in GX & X meets Y )
thus  Z = X by A7; ::_thesis: ( X in GX & X meets Y )
thus  X in GX by A1, A8; ::_thesis: X meets Y
thus  X meets Y by A9; ::_thesis: verum
end;
hence  Z in  {  X where X is Subset of T : ( X in GX & X meets Y )  }  ; ::_thesis: verum
end;
hence   {  V where V is Subset of T : ( V in FX & V meets W )  }  c=  {  X where X is Subset of T : ( X in GX & X meets Y )  }  by TARSKI:def_3; ::_thesis: verum
end;
hence   {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite by A5; ::_thesis: verum
end;
end;
hence  FX is locally_finite by Def1; ::_thesis: verum
end;

theorem Th10: :: PCOMPS_1:10
for T being non empty TopSpace
for FX being Subset-Family of T st FX is finite holds
FX is locally_finite
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is finite holds
FX is locally_finite
let FX be Subset-Family of T; ::_thesis: ( FX is finite implies FX is locally_finite )
assume A1: FX is finite ; ::_thesis: FX is locally_finite
 for x being Point of T ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite )
proof
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite )
take  [#] T ; ::_thesis: ( x in [#] T & [#] T is open &  {  V where V is Subset of T : ( V in FX & V meets [#] T )  }  is finite )
thus  x in [#] T ; ::_thesis: ( [#] T is open &  {  V where V is Subset of T : ( V in FX & V meets [#] T )  }  is finite )
thus  [#] T is open ; ::_thesis:  {  V where V is Subset of T : ( V in FX & V meets [#] T )  }  is finite
thus   {  V where V is Subset of T : ( V in FX & V meets [#] T )  }  is finite by A1, Th8, FINSET_1:1; ::_thesis: verum
end;
hence  FX is locally_finite by Def1; ::_thesis: verum
end;

definition
let T be TopStruct ;
let FX be Subset-Family of T;
func clf FX ->  Subset-Family of T means :Def2: :: PCOMPS_1:def 2
 for Z being Subset of T holds
( Z in it iff ex W being Subset of T st
( Z = Cl W & W in FX ) );
existence
 ex b1 being Subset-Family of T st
for Z being Subset of T holds
( Z in b1 iff ex W being Subset of T st
( Z = Cl W & W in FX ) )
proof
defpred S1[ set ] means  ex W being Subset of T st
( $1 = Cl W & W in FX );
thus  ex S being Subset-Family of T st
for Z being Subset of T holds
( Z in S iff S1[Z] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of T st ( for Z being Subset of T holds
( Z in b1 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds
( Z in b2 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) holds
b1 = b2
proof
let HX, GX be Subset-Family of T; ::_thesis: ( ( for Z being Subset of T holds
( Z in HX iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) & ( for Z being Subset of T holds
( Z in GX iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) ) implies HX = GX )
assume that
A1: for Z being Subset of T holds
( Z in HX iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) and
A2: for X being Subset of T holds
( X in GX iff ex V being Subset of T st
( X = Cl V & V in FX ) ) ; ::_thesis: HX = GX
now__::_thesis:_for_X_being_set_st_X_in_GX_holds_
X_in_HX
let X be set ; ::_thesis: ( X in GX implies X in HX )
assume A3: X in GX ; ::_thesis: X in HX
then reconsider X9 = X as Subset of T ;
 ex V being Subset of T st
( X9 = Cl V & V in FX ) by A2, A3;
hence  X in HX by A1; ::_thesis: verum
end;
then A4: GX c= HX by TARSKI:def_3;
now__::_thesis:_for_Z_being_set_st_Z_in_HX_holds_
Z_in_GX
let Z be set ; ::_thesis: ( Z in HX implies Z in GX )
assume A5: Z in HX ; ::_thesis: Z in GX
then reconsider Z9 = Z as Subset of T ;
 ex W being Subset of T st
( Z9 = Cl W & W in FX ) by A1, A5;
hence  Z in GX by A2; ::_thesis: verum
end;
then  HX c= GX by TARSKI:def_3;
hence  HX = GX by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines clf PCOMPS_1:def_2_:_
 for T being TopStruct
for FX, b3 being Subset-Family of T holds
( b3 = clf FX iff for Z being Subset of T holds
( Z in b3 iff ex W being Subset of T st
( Z = Cl W & W in FX ) ) );

theorem :: PCOMPS_1:11
for T being TopSpace
for FX being Subset-Family of T holds clf FX is closed
proof
let T be TopSpace; ::_thesis: for FX being Subset-Family of T holds clf FX is closed
let FX be Subset-Family of T; ::_thesis: clf FX is closed
 for V being Subset of T st V in clf FX holds
V is closed
proof
let V be Subset of T; ::_thesis: ( V in clf FX implies V is closed )
assume  V in clf FX ; ::_thesis: V is closed
then  ex W being Subset of T st
( V = Cl W & W in FX ) by Def2;
hence  V is closed ; ::_thesis: verum
end;
hence  clf FX is closed by TOPS_2:def_2; ::_thesis: verum
end;

theorem Th12: :: PCOMPS_1:12
for T being TopSpace
for FX being Subset-Family of T st FX = {} holds
clf FX = {}
proof
let T be TopSpace; ::_thesis: for FX being Subset-Family of T st FX = {} holds
clf FX = {}
let FX be Subset-Family of T; ::_thesis: ( FX = {} implies clf FX = {} )
reconsider CFX = clf FX as set ;
set X = the Element of CFX;
assume A1: FX = {} ; ::_thesis: clf FX = {}
A2: for X being set holds not X in CFX
proof
let X be set ; ::_thesis: not X in CFX
assume A3: X in CFX ; ::_thesis: contradiction
then reconsider X = X as Subset of T ;
 ex V being Subset of T st
( X = Cl V & V in FX ) by A3, Def2;
hence  contradiction by A1; ::_thesis: verum
end;
assume  not clf FX = {} ; ::_thesis: contradiction
then  the Element of CFX in CFX ;
hence  contradiction by A2; ::_thesis: verum
end;

theorem Th13: :: PCOMPS_1:13
for T being non empty TopSpace
for V being Subset of T
for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
proof
let T be non empty TopSpace; ::_thesis: for V being Subset of T
for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
let V be Subset of T; ::_thesis: for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
let FX be Subset-Family of T; ::_thesis: ( FX = {V} implies clf FX = {(Cl V)} )
reconsider CFX = clf FX as set ;
assume A1: FX = {V} ; ::_thesis: clf FX = {(Cl V)}
 for W being set holds
( W in CFX iff W = Cl V )
proof
let W be set ; ::_thesis: ( W in CFX iff W = Cl V )
A2: ( W = Cl V implies W in CFX )
proof
assume A3: W = Cl V ; ::_thesis: W in CFX
 ex X being Subset of T st
( W = Cl X & X in FX )
proof
take  V ; ::_thesis: ( W = Cl V & V in FX )
thus  ( W = Cl V & V in FX ) by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
hence  W in CFX by Def2; ::_thesis: verum
end;
 ( W in CFX implies W = Cl V )
proof
assume A4: W in CFX ; ::_thesis: W = Cl V
then reconsider W = W as Subset of T ;
 ex X being Subset of T st
( W = Cl X & X in FX ) by A4, Def2;
hence  W = Cl V by A1, TARSKI:def_1; ::_thesis: verum
end;
hence  ( W in CFX iff W = Cl V ) by A2; ::_thesis: verum
end;
hence  clf FX = {(Cl V)} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th14: :: PCOMPS_1:14
for T being non empty TopSpace
for FX, GX being Subset-Family of T st FX c= GX holds
clf FX c= clf GX
proof
let T be non empty TopSpace; ::_thesis: for FX, GX being Subset-Family of T st FX c= GX holds
clf FX c= clf GX
let FX, GX be Subset-Family of T; ::_thesis: ( FX c= GX implies clf FX c= clf GX )
reconsider CFX = clf FX, CGX = clf GX as set ;
assume A1: FX c= GX ; ::_thesis: clf FX c= clf GX
 for X being set st X in CFX holds
X in CGX
proof
let X be set ; ::_thesis: ( X in CFX implies X in CGX )
assume A2: X in CFX ; ::_thesis: X in CGX
then reconsider X = X as Subset of T ;
 ex V being Subset of T st
( X = Cl V & V in FX ) by A2, Def2;
hence  X in CGX by A1, Def2; ::_thesis: verum
end;
hence  clf FX c= clf GX by TARSKI:def_3; ::_thesis: verum
end;

theorem Th15: :: PCOMPS_1:15
for T being non empty TopSpace
for FX, GX being Subset-Family of T holds clf (FX \/ GX) = (clf FX) \/ (clf GX)
proof
let T be non empty TopSpace; ::_thesis: for FX, GX being Subset-Family of T holds clf (FX \/ GX) = (clf FX) \/ (clf GX)
let FX, GX be Subset-Family of T; ::_thesis: clf (FX \/ GX) = (clf FX) \/ (clf GX)
 for X being set holds
( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) )
proof
let X be set ; ::_thesis: ( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) )
A1: now__::_thesis:_(_X_in_(clf_FX)_\/_(clf_GX)_implies_X_in_clf_(FX_\/_GX)_)
assume A2: X in (clf FX) \/ (clf GX) ; ::_thesis: X in clf (FX \/ GX)
now__::_thesis:_X_in_clf_(FX_\/_GX)
percases ( X in clf FX or X in clf GX ) by A2, XBOOLE_0:def_3;
supposeA3: X in clf FX ; ::_thesis: X in clf (FX \/ GX)
then reconsider X9 = X as Subset of T ;
 ex W being Subset of T st
( X9 = Cl W & W in FX \/ GX )
proof
consider Z being Subset of T such that
A4: ( X9 = Cl Z & Z in FX ) by A3, Def2;
take  Z ; ::_thesis: ( X9 = Cl Z & Z in FX \/ GX )
thus  ( X9 = Cl Z & Z in FX \/ GX ) by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  X in clf (FX \/ GX) by Def2; ::_thesis: verum
end;
supposeA5: X in clf GX ; ::_thesis: X in clf (FX \/ GX)
then reconsider X9 = X as Subset of T ;
 ex W being Subset of T st
( X9 = Cl W & W in FX \/ GX )
proof
consider Z being Subset of T such that
A6: ( X9 = Cl Z & Z in GX ) by A5, Def2;
take  Z ; ::_thesis: ( X9 = Cl Z & Z in FX \/ GX )
thus  ( X9 = Cl Z & Z in FX \/ GX ) by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  X in clf (FX \/ GX) by Def2; ::_thesis: verum
end;
end;
end;
hence  X in clf (FX \/ GX) ; ::_thesis: verum
end;
now__::_thesis:_(_X_in_clf_(FX_\/_GX)_implies_X_in_(clf_FX)_\/_(clf_GX)_)
assume A7: X in clf (FX \/ GX) ; ::_thesis: X in (clf FX) \/ (clf GX)
then reconsider X9 = X as Subset of T ;
consider W being Subset of T such that
A8: X9 = Cl W and
A9: W in FX \/ GX by A7, Def2;
now__::_thesis:_X9_in_(clf_FX)_\/_(clf_GX)
percases ( W in FX or W in GX ) by A9, XBOOLE_0:def_3;
suppose W in FX ; ::_thesis: X9 in (clf FX) \/ (clf GX)
then  X9 in clf FX by A8, Def2;
hence  X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose W in GX ; ::_thesis: X9 in (clf FX) \/ (clf GX)
then  X9 in clf GX by A8, Def2;
hence  X9 in (clf FX) \/ (clf GX) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  X in (clf FX) \/ (clf GX) ; ::_thesis: verum
end;
hence  ( X in clf (FX \/ GX) iff X in (clf FX) \/ (clf GX) ) by A1; ::_thesis: verum
end;
hence  clf (FX \/ GX) = (clf FX) \/ (clf GX) by TARSKI:1; ::_thesis: verum
end;

theorem Th16: :: PCOMPS_1:16
for T being non empty TopSpace
for FX being Subset-Family of T st FX is finite holds
Cl (union FX) = union (clf FX)
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is finite holds
Cl (union FX) = union (clf FX)
let FX be Subset-Family of T; ::_thesis: ( FX is finite implies Cl (union FX) = union (clf FX) )
assume  FX is finite ; ::_thesis: Cl (union FX) = union (clf FX)
then consider p being FinSequence such that
A1: rng p = FX by FINSEQ_1:52;
consider n being Nat such that
A2: dom p = Seg n by FINSEQ_1:def_2;
defpred S1[ Nat] means  for GX being Subset-Family of T st GX = p .: (Seg $1) & $1 <= n & 1 <= n holds
Cl (union GX) = union (clf GX);
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: for GX being Subset-Family of T st GX = p .: (Seg k) & k <= n & 1 <= n holds
Cl (union GX) = union (clf GX) ; ::_thesis: S1[k + 1]
let GX be Subset-Family of T; ::_thesis: ( GX = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies Cl (union GX) = union (clf GX) )
assume A5: GX = p .: (Seg (k + 1)) ; ::_thesis: ( not k + 1 <= n or not 1 <= n or Cl (union GX) = union (clf GX) )
assume that
A6: k + 1 <= n and
A7: 1 <= n ; ::_thesis: Cl (union GX) = union (clf GX)
now__::_thesis:_Cl_(union_GX)_=_union_(clf_GX)
reconsider G2 = Im (p,(k + 1)) as Subset-Family of T by A1, RELAT_1:111, TOPS_2:2;
reconsider G1 = p .: (Seg k) as Subset-Family of T by A1, RELAT_1:111, TOPS_2:2;
 k + 1 <= n + 1 by A6, NAT_1:12;
then A8: k <= n by XREAL_1:6;
 0 + 1 = 1 ;
then  1 <= k + 1 by XREAL_1:7;
then  k + 1 in dom p by A2, A6, FINSEQ_1:1;
then A9: G2 = {(p . (k + 1))} by FUNCT_1:59;
then  union G2 = p . (k + 1) by ZFMISC_1:25;
then reconsider G3 = p . (k + 1) as Subset of T ;
A10: union (clf G2) = union {(Cl G3)} by A9, Th13
.= Cl G3 by ZFMISC_1:25
.= Cl (union G2) by A9, ZFMISC_1:25 ;
A11: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ;
then  Cl (union GX) = Cl ((union G1) \/ (union G2)) by A5, ZFMISC_1:78
.= (Cl (union G1)) \/ (Cl (union G2)) by PRE_TOPC:20 ;
then  Cl (union GX) = (union (clf G1)) \/ (union (clf G2)) by A4, A7, A10, A8;
then  Cl (union GX) = union ((clf G1) \/ (clf G2)) by ZFMISC_1:78;
hence  Cl (union GX) = union (clf GX) by A5, A11, Th15; ::_thesis: verum
end;
hence  Cl (union GX) = union (clf GX) ; ::_thesis: verum
end;
A12: S1[ 0 ]
proof
let GX be Subset-Family of T; ::_thesis: ( GX = p .: (Seg 0) & 0 <= n & 1 <= n implies Cl (union GX) = union (clf GX) )
assume that
A13: GX = p .: (Seg 0) and
 0 <= n and
 1 <= n ; ::_thesis: Cl (union GX) = union (clf GX)
 union GX = {} T by A13, ZFMISC_1:2;
then  Cl (union GX) = {} T by PRE_TOPC:22;
hence  Cl (union GX) = union (clf GX) by A13, Th12, ZFMISC_1:2; ::_thesis: verum
end;
A14: for k being Nat holds S1[k] from NAT_1:sch_2(A12, A3);
A15: now__::_thesis:_(_1_<=_n_implies_Cl_(union_FX)_=_union_(clf_FX)_)
assume A16: 1 <= n ; ::_thesis: Cl (union FX) = union (clf FX)
 FX = p .: (Seg n) by A1, A2, RELAT_1:113;
hence  Cl (union FX) = union (clf FX) by A14, A16; ::_thesis: verum
end;
A17: now__::_thesis:_(_n_=_0_implies_Cl_(union_FX)_=_union_(clf_FX)_)
assume  n = 0 ; ::_thesis: Cl (union FX) = union (clf FX)
then  Seg n = {} ;
then A18: FX = p .: {} by A1, A2, RELAT_1:113;
then  union FX = {} T by ZFMISC_1:2;
then  Cl (union FX) = {} T by PRE_TOPC:22;
hence  Cl (union FX) = union (clf FX) by A18, Th12, ZFMISC_1:2; ::_thesis: verum
end;
now__::_thesis:_(_n_<>_0_implies_1_<=_n_)
A19: 1 = 0 + 1 ;
assume  n <> 0 ; ::_thesis: 1 <= n
hence  1 <= n by A19, NAT_1:13; ::_thesis: verum
end;
hence  Cl (union FX) = union (clf FX) by A15, A17; ::_thesis: verum
end;

theorem Th17: :: PCOMPS_1:17
for T being non empty TopSpace
for FX being Subset-Family of T holds FX is_finer_than clf FX
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T holds FX is_finer_than clf FX
let FX be Subset-Family of T; ::_thesis: FX is_finer_than clf FX
set GX = clf FX;
 for X being set st X in FX holds
ex Y being set st
( Y in clf FX & X c= Y )
proof
let X be set ; ::_thesis: ( X in FX implies ex Y being set st
( Y in clf FX & X c= Y ) )
assume A1: X in FX ; ::_thesis: ex Y being set st
( Y in clf FX & X c= Y )
then reconsider X = X as Subset of T ;
thus  ex Y being set st
( Y in clf FX & X c= Y ) ::_thesis: verum
proof
reconsider Y = Cl X as set ;
take  Y ; ::_thesis: ( Y in clf FX & X c= Y )
thus  Y in clf FX by A1, Def2; ::_thesis: X c= Y
thus  X c= Y by PRE_TOPC:18; ::_thesis: verum
end;
end;
hence  FX is_finer_than clf FX by SETFAM_1:def_2; ::_thesis: verum
end;

scheme :: PCOMPS_1:sch 1
Lambda1top{ F1() ->  TopSpace, F2() ->  Subset-Family of F1(), F3() ->  Subset-Family of F1(), F4( set ) ->  Subset of F1() } :
 ex f being Function of F2(),F3() st
for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z)
provided
A1: for Z being Subset of F1() st Z in F2() holds
F4(Z) in F3()
proof
A2: for x being set st x in F2() holds
F4(x) in F3() by A1;
consider f being Function of F2(),F3() such that
A3: for x being set st x in F2() holds
f . x = F4(x) from FUNCT_2:sch_2(A2);
take  f ; ::_thesis: for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z)
thus  for Z being Subset of F1() st Z in F2() holds
f . Z = F4(Z) by A3; ::_thesis: verum
end;

theorem :: PCOMPS_1:18
for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite holds
clf FX is locally_finite
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is locally_finite holds
clf FX is locally_finite
let FX be Subset-Family of T; ::_thesis: ( FX is locally_finite implies clf FX is locally_finite )
set GX = clf FX;
assume A1: FX is locally_finite ; ::_thesis: clf FX is locally_finite
 for x being Point of T ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  is finite )
proof
let x be Point of T; ::_thesis: ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  is finite )
thus  ex W being Subset of T st
( x in W & W is open &  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  is finite ) ::_thesis: verum
proof
deffunc H1( Subset of T) ->  Element of bool the carrier of T = Cl $1;
consider W being Subset of T such that
A2: x in W and
A3: W is open and
A4:  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite by A1, Def1;
take  W ; ::_thesis: ( x in W & W is open &  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  is finite )
thus  x in W by A2; ::_thesis: ( W is open &  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  is finite )
thus  W is open by A3; ::_thesis:  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  is finite
set CGX =  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  ;
set CFX =  {  V where V is Subset of T : ( V in FX & V meets W )  }  ;
A5: for Y being Subset of T st Y in FX holds
H1(Y) in clf FX by Def2;
consider f being Function of FX,(clf FX) such that
A6: for X being Subset of T st X in FX holds
f . X = H1(X) from PCOMPS_1:sch_1(A5);
A7: ( clf FX = {} implies FX = {} ) by Th17, SETFAM_1:16;
then A8: dom f = FX by FUNCT_2:def_1;
 for Z being set holds
( Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }  iff Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  )
proof
let Z be set ; ::_thesis: ( Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }  iff Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  )
A9: ( Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  implies Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }  )
proof
assume A10: Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  ; ::_thesis: Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }
 ex Y being set st
( Y in dom f & Y in  {  V where V is Subset of T : ( V in FX & V meets W )  }  & Z = f . Y )
proof
consider V being Subset of T such that
A11: Z = V and
A12: V in clf FX and
A13: V meets W by A10;
consider X being Subset of T such that
A14: V = Cl X and
A15: X in FX by A12, Def2;
take  X ; ::_thesis: ( X in dom f & X in  {  V where V is Subset of T : ( V in FX & V meets W )  }  & Z = f . X )
A16: V /\ W <> {} by A13, XBOOLE_0:def_7;
 ex Q being Subset of T st
( X = Q & Q in FX & Q meets W )
proof
take Q = X; ::_thesis: ( X = Q & Q in FX & Q meets W )
thus  X = Q ; ::_thesis: ( Q in FX & Q meets W )
thus  Q in FX by A15; ::_thesis: Q meets W
 Cl (W /\ (Cl Q)) <> {} by A16, A14, Th2;
then  Cl (W /\ Q) <> {} by A3, TOPS_1:14;
then  Q /\ W <> {} by Th2;
hence  Q meets W by XBOOLE_0:def_7; ::_thesis: verum
end;
hence  ( X in dom f & X in  {  V where V is Subset of T : ( V in FX & V meets W )  }  & Z = f . X ) by A6, A7, A11, A14, FUNCT_2:def_1; ::_thesis: verum
end;
hence  Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }  by FUNCT_1:def_6; ::_thesis: verum
end;
 ( Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }  implies Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  )
proof
assume  Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }  ; ::_thesis: Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }
then consider Y being set  such that
A17: Y in dom f and
A18: Y in  {  V where V is Subset of T : ( V in FX & V meets W )  }  and
A19: Z = f . Y by FUNCT_1:def_6;
reconsider Y = Y as Subset of T by A8, A17;
A20: f . Y = Cl Y by A6, A8, A17;
then reconsider Z = Z as Subset of T by A19;
 ex V being Subset of T st
( Y = V & V in FX & V meets W ) by A18;
then A21: Z meets W by A19, A20, PRE_TOPC:18, XBOOLE_1:63;
 Z in clf FX by A8, A17, A19, A20, Def2;
hence  Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  by A21; ::_thesis: verum
end;
hence  ( Z in f .:  {  V where V is Subset of T : ( V in FX & V meets W )  }  iff Z in  {  V where V is Subset of T : ( V in clf FX & V meets W )  }  ) by A9; ::_thesis: verum
end;
hence   {  V where V is Subset of T : ( V in clf FX & V meets W )  }  is finite by A4, TARSKI:1; ::_thesis: verum
end;
end;
hence  clf FX is locally_finite by Def1; ::_thesis: verum
end;

theorem :: PCOMPS_1:19
for T being non empty TopSpace
for FX being Subset-Family of T holds union FX c= union (clf FX) by Th17, SETFAM_1:13;

theorem Th20: :: PCOMPS_1:20
for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite holds
Cl (union FX) = union (clf FX)
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is locally_finite holds
Cl (union FX) = union (clf FX)
let FX be Subset-Family of T; ::_thesis: ( FX is locally_finite implies Cl (union FX) = union (clf FX) )
set UFX = Cl (union FX);
set UCFX = union (clf FX);
assume A1: FX is locally_finite ; ::_thesis: Cl (union FX) = union (clf FX)
 for x being Point of T st x in Cl (union FX) holds
x in union (clf FX)
proof
let x be Point of T; ::_thesis: ( x in Cl (union FX) implies x in union (clf FX) )
consider W being Subset of T such that
A2: ( x in W & W is open ) and
A3:  {  V where V is Subset of T : ( V in FX & V meets W )  }  is finite by A1, Def1;
set HX =  {  V where V is Subset of T : ( V in FX & V meets W )  }  ;
reconsider HX =  {  V where V is Subset of T : ( V in FX & V meets W )  }  as Subset-Family of T by Th8, TOPS_2:2;
A4: Cl (union HX) = union (clf HX) by A3, Th16;
set FHX = FX \ HX;
A5: not x in Cl (union (FX \ HX))
proof
assume A6: x in Cl (union (FX \ HX)) ; ::_thesis: contradiction
reconsider FHX = FX \ HX as set ;
 for Z being set st Z in FHX holds
Z misses W
proof
let Z be set ; ::_thesis: ( Z in FHX implies Z misses W )
assume A7: Z in FHX ; ::_thesis: Z misses W
then reconsider Z = Z as Subset of T ;
 ( Z in FX & not Z in HX ) by A7, XBOOLE_0:def_5;
hence  Z misses W ; ::_thesis: verum
end;
then  union FHX misses W by ZFMISC_1:80;
hence  contradiction by A2, A6, TOPS_1:12; ::_thesis: verum
end;
HX \/ (FX \ HX) = HX \/ FX by XBOOLE_1:39
.= FX by Th8, XBOOLE_1:12 ;
then A8: Cl (union FX) = Cl ((union HX) \/ (union (FX \ HX))) by ZFMISC_1:78
.= (Cl (union HX)) \/ (Cl (union (FX \ HX))) by PRE_TOPC:20 ;
 clf HX c= clf FX by Th8, Th14;
then A9: union (clf HX) c= union (clf FX) by ZFMISC_1:77;
assume  x in Cl (union FX) ; ::_thesis: x in union (clf FX)
then  x in Cl (union HX) by A5, A8, XBOOLE_0:def_3;
hence  x in union (clf FX) by A4, A9; ::_thesis: verum
end;
then A10: Cl (union FX) c= union (clf FX) by SUBSET_1:2;
 for x being Point of T st x in union (clf FX) holds
x in Cl (union FX)
proof
let x be Point of T; ::_thesis: ( x in union (clf FX) implies x in Cl (union FX) )
assume  x in union (clf FX) ; ::_thesis: x in Cl (union FX)
then consider X being set  such that
A11: x in X and
A12: X in clf FX by TARSKI:def_4;
reconsider X = X as Subset of T by A12;
consider Y being Subset of T such that
A13: X = Cl Y and
A14: Y in FX by A12, Def2;
 for A being Subset of T st A is open & x in A holds
union FX meets A
proof
let A be Subset of T; ::_thesis: ( A is open & x in A implies union FX meets A )
assume A15: ( A is open & x in A ) ; ::_thesis: union FX meets A
 ex y being Point of T st y in (union FX) /\ A
proof
 Y meets A by A11, A13, A15, TOPS_1:12;
then consider z being set  such that
A16: z in Y /\ A by XBOOLE_0:4;
 z in Y by A16, XBOOLE_0:def_4;
then A17: z in union FX by A14, TARSKI:def_4;
take  z ; ::_thesis: ( z is Point of T & z in (union FX) /\ A )
 z in A by A16, XBOOLE_0:def_4;
hence  ( z is Point of T & z in (union FX) /\ A ) by A17, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  union FX meets A by XBOOLE_0:4; ::_thesis: verum
end;
hence  x in Cl (union FX) by TOPS_1:12; ::_thesis: verum
end;
then  union (clf FX) c= Cl (union FX) by SUBSET_1:2;
hence  Cl (union FX) = union (clf FX) by A10, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: PCOMPS_1:21
for T being non empty TopSpace
for FX being Subset-Family of T st FX is locally_finite & FX is closed holds
union FX is closed
proof
let T be non empty TopSpace; ::_thesis: for FX being Subset-Family of T st FX is locally_finite & FX is closed holds
union FX is closed
let FX be Subset-Family of T; ::_thesis: ( FX is locally_finite & FX is closed implies union FX is closed )
assume that
A1: FX is locally_finite and
A2: FX is closed ; ::_thesis: union FX is closed
 union (clf FX) c= union FX
proof
set UFX = union FX;
set UCFX = union (clf FX);
 for x being Point of T st x in union (clf FX) holds
x in union FX
proof
let x be Point of T; ::_thesis: ( x in union (clf FX) implies x in union FX )
assume  x in union (clf FX) ; ::_thesis: x in union FX
then consider X being set  such that
A3: x in X and
A4: X in clf FX by TARSKI:def_4;
reconsider X = X as Subset of T by A4;
consider W being Subset of T such that
A5: X = Cl W and
A6: W in FX by A4, Def2;
reconsider W = W as Subset of T ;
 W is closed by A2, A6, TOPS_2:def_2;
then  x in W by A3, A5, PRE_TOPC:22;
hence  x in union FX by A6, TARSKI:def_4; ::_thesis: verum
end;
hence  union (clf FX) c= union FX by SUBSET_1:2; ::_thesis: verum
end;
then A7: Cl (union FX) c= union FX by A1, Th20;
 union FX c= union (clf FX) by Th17, SETFAM_1:13;
then  union FX c= Cl (union FX) by A1, Th20;
hence  union FX is closed by A7, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let IT be TopStruct ;
attrIT is paracompact  means :Def3: :: PCOMPS_1:def 3
 for FX being Subset-Family of IT st FX is Cover of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite );
end;

:: deftheorem Def3 defines paracompact PCOMPS_1:def_3_:_
 for IT being TopStruct holds
( IT is paracompact iff for FX being Subset-Family of IT st FX is Cover of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite ) );

registration
cluster non empty TopSpace-like paracompact for TopStruct ;
existence
 ex b1 being non empty TopSpace st b1 is paracompact
proof
take PT = 1TopSp {1}; ::_thesis: PT is paracompact
let FX be Subset-Family of PT; :: according to PCOMPS_1:def_3 ::_thesis: ( FX is Cover of PT & FX is open implies ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) )
assume that
A1: FX is Cover of PT and
 FX is open ; ::_thesis: ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
consider GX being Subset-Family of PT such that
A2: ( GX c= FX & GX is Cover of PT ) and
 GX is finite by A1;
take  GX ; ::_thesis: ( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
thus  ( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) by A2, Th10, SETFAM_1:12, TOPS_2:11; ::_thesis: verum
end;
end;

theorem :: PCOMPS_1:22
for T being non empty TopSpace st T is compact holds
T is paracompact
proof
let T be non empty TopSpace; ::_thesis: ( T is compact implies T is paracompact )
assume A1: T is compact ; ::_thesis: T is paracompact
 for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
proof
let FX be Subset-Family of T; ::_thesis: ( FX is Cover of T & FX is open implies ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite ) )
assume that
A2: FX is Cover of T and
A3: FX is open ; ::_thesis: ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
consider GX being Subset-Family of T such that
A4: GX c= FX and
A5: GX is Cover of T and
A6: GX is finite by A1, A2, A3, COMPTS_1:def_1;
take  GX ; ::_thesis: ( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
 for W being Subset of T st W in GX holds
W is open by A3, A4, TOPS_2:def_1;
hence  GX is open by TOPS_2:def_1; ::_thesis: ( GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
thus  GX is Cover of T by A5; ::_thesis: ( GX is_finer_than FX & GX is locally_finite )
thus  GX is_finer_than FX by A4, SETFAM_1:12; ::_thesis: GX is locally_finite
thus  GX is locally_finite by A6, Th10; ::_thesis: verum
end;
hence  T is paracompact by Def3; ::_thesis: verum
end;

theorem Th23: :: PCOMPS_1:23
for T being non empty TopSpace
for B, A being Subset of T st T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) holds
ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
proof
let T be non empty TopSpace; ::_thesis: for B, A being Subset of T st T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) holds
ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
let B, A be Subset of T; ::_thesis: ( T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) implies ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) )
assume that
A1: T is paracompact and
A2: B is closed and
A3: for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ; ::_thesis: ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
defpred S1[ set ] means ( $1 = B ` or ex V, W being Subset of T ex x being Point of T st
( x in B & $1 = W & V is open & W is open & A c= V & x in W & V misses W ) );
consider GX being Subset-Family of T such that
A4: for X being Subset of T holds
( X in GX iff S1[X] ) from SUBSET_1:sch_3();
now__::_thesis:_for_x_being_Point_of_T_st_x_in_[#]_T_holds_
x_in_union_GX
let x be Point of T; ::_thesis: ( x in [#] T implies x in union GX )
assume  x in [#] T ; ::_thesis: x in union GX
then A5: x in B \/ (B `) by PRE_TOPC:2;
now__::_thesis:_x_in_union_GX
percases ( x in B or x in B ` ) by A5, XBOOLE_0:def_3;
supposeA6: x in B ; ::_thesis: x in union GX
 ex X being Subset of T st
( x in X & X in GX )
proof
consider V, W being Subset of T such that
A7: ( V is open & W is open & A c= V ) and
A8: x in W and
A9: V misses W by A3, A6;
take X = W; ::_thesis: ( x in X & X in GX )
thus  x in X by A8; ::_thesis: X in GX
thus  X in GX by A4, A6, A7, A8, A9; ::_thesis: verum
end;
hence  x in union GX by TARSKI:def_4; ::_thesis: verum
end;
supposeA10: x in B ` ; ::_thesis: x in union GX
 ex X being Subset of T st
( x in X & X in GX )
proof
take X = B ` ; ::_thesis: ( x in X & X in GX )
thus  x in X by A10; ::_thesis: X in GX
thus  X in GX by A4; ::_thesis: verum
end;
hence  x in union GX by TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence  x in union GX ; ::_thesis: verum
end;
then  [#] T c= union GX by SUBSET_1:2;
then  [#] T = union GX by XBOOLE_0:def_10;
then A11: GX is Cover of T by SETFAM_1:45;
 for X being Subset of T st X in GX holds
X is open
proof
let X be Subset of T; ::_thesis: ( X in GX implies X is open )
assume A12: X in GX ; ::_thesis: X is open
now__::_thesis:_X_is_open
percases ( X = B ` or ex V, W being Subset of T ex y being Point of T st
( y in B & X = W & V is open & W is open & A c= V & y in W & V misses W ) ) by A4, A12;
suppose X = B ` ; ::_thesis: X is open
hence  X is open by A2; ::_thesis: verum
end;
suppose ex V, W being Subset of T ex y being Point of T st
( y in B & X = W & V is open & W is open & A c= V & y in W & V misses W ) ; ::_thesis: X is open
hence  X is open ; ::_thesis: verum
end;
end;
end;
hence  X is open ; ::_thesis: verum
end;
then  GX is open by TOPS_2:def_1;
then consider FX being Subset-Family of T such that
A13: FX is open and
A14: FX is Cover of T and
A15: FX is_finer_than GX and
A16: FX is locally_finite by A1, A11, Def3;
set HX =  {  W where W is Subset of T : ( W in FX & W meets B )  }  ;
A17:  {  W where W is Subset of T : ( W in FX & W meets B )  }  c= FX by Th8;
reconsider HX =  {  W where W is Subset of T : ( W in FX & W meets B )  }  as Subset-Family of T by Th8, TOPS_2:2;
take Y = (union (clf HX)) ` ; ::_thesis: ex Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
take Z = union HX; ::_thesis: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
 union (clf HX) = Cl (union HX) by A16, A17, Th9, Th20;
hence  Y is open ; ::_thesis: ( Z is open & A c= Y & B c= Z & Y misses Z )
thus  Z is open by A13, A17, TOPS_2:11, TOPS_2:19; ::_thesis: ( A c= Y & B c= Z & Y misses Z )
A18: for X being Subset of T st X in HX holds
A /\ (Cl X) = {}
proof
let X be Subset of T; ::_thesis: ( X in HX implies A /\ (Cl X) = {} )
assume  X in HX ; ::_thesis: A /\ (Cl X) = {}
then A19: ex W being Subset of T st
( W = X & W in FX & W meets B ) ;
then consider Y being set  such that
A20: Y in GX and
A21: X c= Y by A15, SETFAM_1:def_2;
reconsider Y = Y as Subset of T by A20;
now__::_thesis:_A_/\_(Cl_X)_=_{}
percases ( Y = B ` or ex V, W being Subset of T ex y being Point of T st
( y in B & Y = W & V is open & W is open & A c= V & y in W & V misses W ) ) by A4, A20;
suppose Y = B ` ; ::_thesis: A /\ (Cl X) = {}
hence  A /\ (Cl X) = {} by A19, A21, XBOOLE_1:63, XBOOLE_1:79; ::_thesis: verum
end;
suppose ex V, W being Subset of T ex y being Point of T st
( y in B & Y = W & V is open & W is open & A c= V & y in W & V misses W ) ; ::_thesis: A /\ (Cl X) = {}
then consider V, W being Subset of T, y being Point of T such that
 y in B and
A22: Y = W and
A23: V is open and
 W is open and
A24: A c= V and
 y in W and
A25: V misses W ;
 V misses X by A21, A22, A25, XBOOLE_1:63;
then  Cl (V /\ X) = Cl ({} T) by XBOOLE_0:def_7;
then  Cl (V /\ X) = {} by PRE_TOPC:22;
then  Cl (V /\ (Cl X)) = {} by A23, TOPS_1:14;
then  V /\ (Cl X) = {} by Th2;
then  Cl X misses V by XBOOLE_0:def_7;
then  A misses Cl X by A24, XBOOLE_1:63;
hence  A /\ (Cl X) = {} by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence  A /\ (Cl X) = {} ; ::_thesis: verum
end;
 A misses union (clf HX)
proof
assume  A meets union (clf HX) ; ::_thesis: contradiction
then consider x being set  such that
A26: x in A and
A27: x in union (clf HX) by XBOOLE_0:3;
reconsider x = x as Point of T by A26;
now__::_thesis:_(_x_in_union_(clf_HX)_implies_not_x_in_A_)
assume  x in union (clf HX) ; ::_thesis: not x in A
then consider X being set  such that
A28: x in X and
A29: X in clf HX by TARSKI:def_4;
reconsider X = X as Subset of T by A29;
 ex W being Subset of T st
( X = Cl W & W in HX ) by A29, Def2;
then  A /\ X = {} by A18;
then  A misses X by XBOOLE_0:def_7;
hence  not x in A by A28, XBOOLE_0:3; ::_thesis: verum
end;
hence  contradiction by A26, A27; ::_thesis: verum
end;
hence  A c= Y by SUBSET_1:23; ::_thesis: ( B c= Z & Y misses Z )
now__::_thesis:_for_y_being_Point_of_T_st_y_in_B_holds_
y_in_Z
let y be Point of T; ::_thesis: ( y in B implies y in Z )
assume A30: y in B ; ::_thesis: y in Z
 ex W being Subset of T st
( y in W & W in HX )
proof
consider W being Subset of T such that
A31: y in W and
A32: W in FX by A14, Th3;
take  W ; ::_thesis: ( y in W & W in HX )
thus  y in W by A31; ::_thesis: W in HX
 W meets B by A30, A31, XBOOLE_0:3;
hence  W in HX by A32; ::_thesis: verum
end;
hence  y in Z by TARSKI:def_4; ::_thesis: verum
end;
hence  B c= Z by SUBSET_1:2; ::_thesis: Y misses Z
 Z c= Y ` by Th17, SETFAM_1:13;
hence  Y misses Z by SUBSET_1:23; ::_thesis: verum
end;

theorem Th24: :: PCOMPS_1:24
for T being non empty TopSpace st T is T_2 & T is paracompact holds
T is regular
proof
let T be non empty TopSpace; ::_thesis: ( T is T_2 & T is paracompact implies T is regular )
assume A1: T is T_2 ; ::_thesis: ( not T is paracompact or T is regular )
assume A2: T is paracompact ; ::_thesis: T is regular
 for x being Point of T
for A being Subset of T st A <> {} & A is closed & x in A ` holds
ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
proof
let x be Point of T; ::_thesis: for A being Subset of T st A <> {} & A is closed & x in A ` holds
ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
let A be Subset of T; ::_thesis: ( A <> {} & A is closed & x in A ` implies ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V ) )
assume that
 A <> {} and
A3: A is closed and
A4: x in A ` ; ::_thesis: ex W, V being Subset of T st
( W is open & V is open & x in W & A c= V & W misses V )
set B = {x};
A5: not x in A by A4, XBOOLE_0:def_5;
 for y being Point of T st y in A holds
ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
proof
let y be Point of T; ::_thesis: ( y in A implies ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W ) )
assume  y in A ; ::_thesis: ex V, W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
then consider V, W being Subset of T such that
A6: ( V is open & W is open & x in V & y in W & V misses W ) by A1, A5, PRE_TOPC:def_10;
take  V ; ::_thesis: ex W being Subset of T st
( V is open & W is open & {x} c= V & y in W & V misses W )
take  W ; ::_thesis: ( V is open & W is open & {x} c= V & y in W & V misses W )
thus  ( V is open & W is open & {x} c= V & y in W & V misses W ) by A6, ZFMISC_1:31; ::_thesis: verum
end;
then consider Y, Z being Subset of T such that
A7: ( Y is open & Z is open & {x} c= Y & A c= Z & Y misses Z ) by A2, A3, Th23;
take  Y ; ::_thesis: ex V being Subset of T st
( Y is open & V is open & x in Y & A c= V & Y misses V )
take  Z ; ::_thesis: ( Y is open & Z is open & x in Y & A c= Z & Y misses Z )
thus  ( Y is open & Z is open & x in Y & A c= Z & Y misses Z ) by A7, ZFMISC_1:31; ::_thesis: verum
end;
hence  T is regular by COMPTS_1:def_2; ::_thesis: verum
end;

theorem :: PCOMPS_1:25
for T being non empty TopSpace st T is T_2 & T is paracompact holds
T is normal
proof
let T be non empty TopSpace; ::_thesis: ( T is T_2 & T is paracompact implies T is normal )
assume that
A1: T is T_2 and
A2: T is paracompact ; ::_thesis: T is normal
 for A, B being Subset of T st A <> {} & B <> {} & A is closed & B is closed & A misses B holds
ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V )
proof
let A, B be Subset of T; ::_thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V ) )
assume that
A3: A <> {} and
 B <> {} and
A4: A is closed and
A5: B is closed and
A6: A misses B ; ::_thesis: ex W, V being Subset of T st
( W is open & V is open & A c= W & B c= V & W misses V )
 for x being Point of T st x in B holds
ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
proof
let x be Point of T; ::_thesis: ( x in B implies ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V ) )
assume  x in B ; ::_thesis: ex W, V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
then  not x in A by A6, XBOOLE_0:3;
then A7: x in A ` by SUBSET_1:29;
 T is regular by A1, A2, Th24;
then consider V, W being Subset of T such that
A8: ( V is open & W is open & x in V & A c= W & V misses W ) by A3, A4, A7, COMPTS_1:def_2;
take  W ; ::_thesis: ex V being Subset of T st
( W is open & V is open & A c= W & x in V & W misses V )
take  V ; ::_thesis: ( W is open & V is open & A c= W & x in V & W misses V )
thus  ( W is open & V is open & A c= W & x in V & W misses V ) by A8; ::_thesis: verum
end;
then consider Y, Z being Subset of T such that
A9: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A2, A5, Th23;
take  Y ; ::_thesis: ex V being Subset of T st
( Y is open & V is open & A c= Y & B c= V & Y misses V )
take  Z ; ::_thesis: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
thus  ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) by A9; ::_thesis: verum
end;
hence  T is normal by COMPTS_1:def_3; ::_thesis: verum
end;


definition
let PM be MetrStruct ;
func Family_open_set PM ->  Subset-Family of PM means :Def4: :: PCOMPS_1:def 4
 for V being Subset of PM holds
( V in it iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) );
existence
 ex b1 being Subset-Family of PM st
for V being Subset of PM holds
( V in b1 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
proof
defpred S1[ set ] means  for x being Element of PM st x in $1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= $1 );
thus  ex S being Subset-Family of PM st
for V being Subset of PM holds
( V in S iff S1[V] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of PM st ( for V being Subset of PM holds
( V in b1 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) & ( for V being Subset of PM holds
( V in b2 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) holds
b1 = b2
proof
let FX, GX be Subset-Family of PM; ::_thesis: ( ( for V being Subset of PM holds
( V in FX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) & ( for V being Subset of PM holds
( V in GX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ) implies FX = GX )
assume A1: for V being Subset of PM holds
( V in FX iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) ; ::_thesis: ( ex V being Subset of PM st
( ( V in GX implies for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) implies ( ( for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) & not V in GX ) ) or FX = GX )
assume A2: for W being Subset of PM holds
( W in GX iff for y being Element of PM st y in W holds
ex p being Real st
( p > 0 & Ball (y,p) c= W ) ) ; ::_thesis: FX = GX
 for Y being Subset of PM holds
( Y in FX iff Y in GX )
proof
let Y be Subset of PM; ::_thesis: ( Y in FX iff Y in GX )
A3: now__::_thesis:_(_Y_in_GX_implies_Y_in_FX_)
assume  Y in GX ; ::_thesis: Y in FX
then  for x being Element of PM st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A2;
hence  Y in FX by A1; ::_thesis: verum
end;
now__::_thesis:_(_Y_in_FX_implies_Y_in_GX_)
assume  Y in FX ; ::_thesis: Y in GX
then  for x being Element of PM st x in Y holds
ex r being Real st
( r > 0 & Ball (x,r) c= Y ) by A1;
hence  Y in GX by A2; ::_thesis: verum
end;
hence  ( Y in FX iff Y in GX ) by A3; ::_thesis: verum
end;
hence  FX = GX by SETFAM_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Family_open_set PCOMPS_1:def_4_:_
 for PM being MetrStruct
for b2 being Subset-Family of PM holds
( b2 = Family_open_set PM iff for V being Subset of PM holds
( V in b2 iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) );

theorem Th26: :: PCOMPS_1:26
for PM being MetrStruct
for x being Element of PM ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
proof
let PM be MetrStruct ; ::_thesis: for x being Element of PM ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
let x be Element of PM; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
consider r being Real such that
A1: r = 1 ;
take  r ; ::_thesis: ( r > 0 & Ball (x,r) c= the carrier of PM )
thus  r > 0 by A1; ::_thesis: Ball (x,r) c= the carrier of PM
thus  Ball (x,r) c= the carrier of PM ; ::_thesis: verum
end;

theorem Th27: :: PCOMPS_1:27
for PM being MetrStruct
for y, x being Element of PM
for r being real number st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
proof
let PM be MetrStruct ; ::_thesis: for y, x being Element of PM
for r being real number st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let y, x be Element of PM; ::_thesis: for r being real number st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
let r be real number ; ::_thesis: ( PM is triangle & y in Ball (x,r) implies ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
reconsider r9 = r as Real by XREAL_0:def_1;
assume A1: PM is triangle ; ::_thesis: ( not y in Ball (x,r) or ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) )
assume A2: y in Ball (x,r) ; ::_thesis: ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )
then A3: dist (x,y) < r by METRIC_1:11;
A4: not PM is empty by A2;
thus  ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) ::_thesis: verum
proof
set p = r9 - (dist (x,y));
take  r9 - (dist (x,y)) ; ::_thesis: ( r9 - (dist (x,y)) > 0 & Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r) )
thus  r9 - (dist (x,y)) > 0 by A3, XREAL_1:50; ::_thesis: Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r)
 for z being Element of PM st z in Ball (y,(r9 - (dist (x,y)))) holds
z in Ball (x,r)
proof
let z be Element of PM; ::_thesis: ( z in Ball (y,(r9 - (dist (x,y)))) implies z in Ball (x,r) )
assume  z in Ball (y,(r9 - (dist (x,y)))) ; ::_thesis: z in Ball (x,r)
then  dist (y,z) < r9 - (dist (x,y)) by METRIC_1:11;
then A5: (dist (x,y)) + (dist (y,z)) < r by XREAL_1:20;
 (dist (x,y)) + (dist (y,z)) >= dist (x,z) by A1, METRIC_1:4;
then  dist (x,z) < r by A5, XXREAL_0:2;
hence  z in Ball (x,r) by A4, METRIC_1:11; ::_thesis: verum
end;
hence  Ball (y,(r9 - (dist (x,y)))) c= Ball (x,r) by SUBSET_1:2; ::_thesis: verum
end;
end;

theorem :: PCOMPS_1:28
for PM being MetrStruct
for r, p being Real
for y, x, z being Element of PM st PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) holds
ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
proof
let PM be MetrStruct ; ::_thesis: for r, p being Real
for y, x, z being Element of PM st PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) holds
ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
let r, p be Real; ::_thesis: for y, x, z being Element of PM st PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) holds
ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
let y, x, z be Element of PM; ::_thesis: ( PM is triangle & y in (Ball (x,r)) /\ (Ball (z,p)) implies ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) ) )
assume A1: PM is triangle ; ::_thesis: ( not y in (Ball (x,r)) /\ (Ball (z,p)) or ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) ) )
assume A2: y in (Ball (x,r)) /\ (Ball (z,p)) ; ::_thesis: ex q being Real st
( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
then  y in Ball (x,r) by XBOOLE_0:def_4;
then consider s being Real such that
 s > 0 and
A3: Ball (y,s) c= Ball (x,r) by A1, Th27;
 y in Ball (z,p) by A2, XBOOLE_0:def_4;
then consider t being Real such that
 t > 0 and
A4: Ball (y,t) c= Ball (z,p) by A1, Th27;
take q = min (s,t); ::_thesis: ( Ball (y,q) c= Ball (x,r) & Ball (y,q) c= Ball (z,p) )
 Ball (y,q) c= Ball (y,s) by Th1, XXREAL_0:17;
hence  Ball (y,q) c= Ball (x,r) by A3, XBOOLE_1:1; ::_thesis: Ball (y,q) c= Ball (z,p)
 Ball (y,q) c= Ball (y,t) by Th1, XXREAL_0:17;
hence  Ball (y,q) c= Ball (z,p) by A4, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th29: :: PCOMPS_1:29
for PM being MetrStruct
for x being Element of PM
for r being real number st PM is triangle holds
Ball (x,r) in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: for x being Element of PM
for r being real number st PM is triangle holds
Ball (x,r) in Family_open_set PM
let x be Element of PM; ::_thesis: for r being real number st PM is triangle holds
Ball (x,r) in Family_open_set PM
let r be real number ; ::_thesis: ( PM is triangle implies Ball (x,r) in Family_open_set PM )
assume  PM is triangle ; ::_thesis: Ball (x,r) in Family_open_set PM
then  for y being Element of PM st y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) ) by Th27;
hence  Ball (x,r) in Family_open_set PM by Def4; ::_thesis: verum
end;

theorem Th30: :: PCOMPS_1:30
for PM being MetrStruct holds the carrier of PM in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: the carrier of PM in Family_open_set PM
 ( the carrier of PM c= the carrier of PM & ( for y being Element of PM st y in the carrier of PM holds
ex p being Real st
( p > 0 & Ball (y,p) c= the carrier of PM ) ) ) by Th26;
hence  the carrier of PM in Family_open_set PM by Def4; ::_thesis: verum
end;

theorem Th31: :: PCOMPS_1:31
for PM being MetrStruct
for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: for V, W being Subset of PM st V in Family_open_set PM & W in Family_open_set PM holds
V /\ W in Family_open_set PM
let V, W be Subset of PM; ::_thesis: ( V in Family_open_set PM & W in Family_open_set PM implies V /\ W in Family_open_set PM )
assume that
A1: V in Family_open_set PM and
A2: W in Family_open_set PM ; ::_thesis: V /\ W in Family_open_set PM
 for z being Element of PM st z in V /\ W holds
ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W )
proof
let z be Element of PM; ::_thesis: ( z in V /\ W implies ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W ) )
assume A3: z in V /\ W ; ::_thesis: ex q being Real st
( q > 0 & Ball (z,q) c= V /\ W )
then  z in V by XBOOLE_0:def_4;
then consider p being Real such that
A4: p > 0 and
A5: Ball (z,p) c= V by A1, Def4;
 z in W by A3, XBOOLE_0:def_4;
then consider r being Real such that
A6: r > 0 and
A7: Ball (z,r) c= W by A2, Def4;
take q = min (p,r); ::_thesis: ( q > 0 & Ball (z,q) c= V /\ W )
thus  q > 0 by A4, A6, XXREAL_0:15; ::_thesis: Ball (z,q) c= V /\ W
 Ball (z,q) c= Ball (z,r) by Th1, XXREAL_0:17;
then A8: Ball (z,q) c= W by A7, XBOOLE_1:1;
 Ball (z,q) c= Ball (z,p) by Th1, XXREAL_0:17;
then  Ball (z,q) c= V by A5, XBOOLE_1:1;
hence  Ball (z,q) c= V /\ W by A8, XBOOLE_1:19; ::_thesis: verum
end;
hence  V /\ W in Family_open_set PM by Def4; ::_thesis: verum
end;

theorem Th32: :: PCOMPS_1:32
for PM being MetrStruct
for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM
proof
let PM be MetrStruct ; ::_thesis: for A being Subset-Family of PM st A c= Family_open_set PM holds
union A in Family_open_set PM
let A be Subset-Family of PM; ::_thesis: ( A c= Family_open_set PM implies union A in Family_open_set PM )
assume A1: A c= Family_open_set PM ; ::_thesis: union A in Family_open_set PM
 for x being Element of PM st x in union A holds
ex r being Real st
( r > 0 & Ball (x,r) c= union A )
proof
let x be Element of PM; ::_thesis: ( x in union A implies ex r being Real st
( r > 0 & Ball (x,r) c= union A ) )
assume  x in union A ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= union A )
then consider W being set  such that
A2: x in W and
A3: W in A by TARSKI:def_4;
reconsider W = W as Subset of PM by A3;
consider r being Real such that
A4: r > 0 and
A5: Ball (x,r) c= W by A1, A2, A3, Def4;
take  r ; ::_thesis: ( r > 0 & Ball (x,r) c= union A )
thus  r > 0 by A4; ::_thesis: Ball (x,r) c= union A
 W c= union A by A3, ZFMISC_1:74;
hence  Ball (x,r) c= union A by A5, XBOOLE_1:1; ::_thesis: verum
end;
hence  union A in Family_open_set PM by Def4; ::_thesis: verum
end;

theorem Th33: :: PCOMPS_1:33
for PM being MetrStruct holds TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace
proof
let PM be MetrStruct ; ::_thesis: TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace
set T = TopStruct(# the carrier of PM,(Family_open_set PM) #);
A1: for p, q being Subset of TopStruct(# the carrier of PM,(Family_open_set PM) #) st p in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) & q in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) holds
p /\ q in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) by Th31;
 ( the carrier of TopStruct(# the carrier of PM,(Family_open_set PM) #) in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) & ( for a being Subset-Family of TopStruct(# the carrier of PM,(Family_open_set PM) #) st a c= the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) holds
union a in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) ) ) by Th30, Th32;
hence  TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace by A1, PRE_TOPC:def_1; ::_thesis: verum
end;

definition
let PM be MetrStruct ;
func TopSpaceMetr PM ->  TopStruct  equals :: PCOMPS_1:def 5
 TopStruct(# the carrier of PM,(Family_open_set PM) #);
coherence
 TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopStruct ;
end;

:: deftheorem  defines TopSpaceMetr PCOMPS_1:def_5_:_
 for PM being MetrStruct holds TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #);

registration
let PM be MetrStruct ;
cluster TopSpaceMetr PM ->  strict TopSpace-like ;
coherence
 ( TopSpaceMetr PM is strict & TopSpaceMetr PM is TopSpace-like ) by Th33;
end;

registration
let PM be non empty MetrStruct ;
cluster TopSpaceMetr PM ->  non empty ;
coherence
 not TopSpaceMetr PM is empty ;
end;

theorem Th34: :: PCOMPS_1:34
for PM being non empty MetrSpace holds TopSpaceMetr PM is T_2
proof
let PM be non empty MetrSpace; ::_thesis: TopSpaceMetr PM is T_2
set TPS = TopSpaceMetr PM;
 for x, y being Element of (TopSpaceMetr PM) st not x = y holds
ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
proof
let x, y be Element of (TopSpaceMetr PM); ::_thesis: ( not x = y implies ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V ) )
assume A1: not x = y ; ::_thesis: ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
reconsider x = x, y = y as Element of PM ;
set r = (dist (x,y)) / 2;
 dist (x,y) <> 0 by A1, METRIC_1:2;
then  dist (x,y) > 0 by METRIC_1:5;
then A2: (dist (x,y)) / 2 > 0 by XREAL_1:139;
 ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
proof
set V = Ball (y,((dist (x,y)) / 2));
set W = Ball (x,((dist (x,y)) / 2));
A3: ( Ball (x,((dist (x,y)) / 2)) in Family_open_set PM & Ball (y,((dist (x,y)) / 2)) in Family_open_set PM ) by Th29;
reconsider W = Ball (x,((dist (x,y)) / 2)), V = Ball (y,((dist (x,y)) / 2)) as Subset of (TopSpaceMetr PM) ;
A4: for z being set holds not z in W /\ V
proof
let z be set ; ::_thesis: not z in W /\ V
assume A5: z in W /\ V ; ::_thesis: contradiction
then reconsider z = z as Element of PM ;
 z in V by A5, XBOOLE_0:def_4;
then A6: dist (y,z) < (dist (x,y)) / 2 by METRIC_1:11;
 z in W by A5, XBOOLE_0:def_4;
then  dist (x,z) < (dist (x,y)) / 2 by METRIC_1:11;
then  (dist (x,z)) + (dist (y,z)) < ((dist (x,y)) / 2) + ((dist (x,y)) / 2) by A6, XREAL_1:8;
hence  contradiction by METRIC_1:4; ::_thesis: verum
end;
take  W ; ::_thesis: ex V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V )
take  V ; ::_thesis: ( W is open & V is open & x in W & y in V & W misses V )
 ( dist (x,x) = 0 & dist (y,y) = 0 ) by METRIC_1:1;
hence  ( W is open & V is open & x in W & y in V & W misses V ) by A2, A3, A4, METRIC_1:11, PRE_TOPC:def_2, XBOOLE_0:4; ::_thesis: verum
end;
hence  ex W, V being Subset of (TopSpaceMetr PM) st
( W is open & V is open & x in W & y in V & W misses V ) ; ::_thesis: verum
end;
hence  TopSpaceMetr PM is T_2 by PRE_TOPC:def_10; ::_thesis: verum
end;

registration
cluster non empty strict TopSpace-like T_2 for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is T_2 & not b1 is empty & b1 is strict )
proof
set M = the non empty MetrSpace;
take  TopSpaceMetr the non empty MetrSpace ; ::_thesis: ( TopSpaceMetr the non empty MetrSpace is T_2 & not TopSpaceMetr the non empty MetrSpace is empty & TopSpaceMetr the non empty MetrSpace is strict )
thus  ( TopSpaceMetr the non empty MetrSpace is T_2 & not TopSpaceMetr the non empty MetrSpace is empty & TopSpaceMetr the non empty MetrSpace is strict ) by Th34; ::_thesis: verum
end;
end;

definition
let D be set ;
let f be Function of [:D,D:],REAL;
predf is_metric_of D means :Def6: :: PCOMPS_1:def 6
 for a, b, c being Element of D holds
( ( f . (a,b) = 0 implies a = b ) & ( a = b implies f . (a,b) = 0 ) & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) );
end;

:: deftheorem Def6 defines is_metric_of PCOMPS_1:def_6_:_
 for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff for a, b, c being Element of D holds
( ( f . (a,b) = 0 implies a = b ) & ( a = b implies f . (a,b) = 0 ) & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) );

theorem Th35: :: PCOMPS_1:35
for D being set
for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
proof
let D be set ; ::_thesis: for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
let f be Function of [:D,D:],REAL; ::_thesis: ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
set DF = MetrStruct(# D,f #);
A1: ( MetrStruct(# D,f #) is MetrSpace implies f is_metric_of D )
proof
assume  MetrStruct(# D,f #) is MetrSpace ; ::_thesis: f is_metric_of D
then reconsider DF = MetrStruct(# D,f #) as MetrSpace ;
 for a, b, c being Element of DF holds
( ( the distance of DF . (a,b) = 0 implies a = b ) & ( a = b implies the distance of DF . (a,b) = 0 ) & the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
proof
let a, b, c be Element of DF; ::_thesis: ( ( the distance of DF . (a,b) = 0 implies a = b ) & ( a = b implies the distance of DF . (a,b) = 0 ) & the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
A2: the distance of DF . (a,b) = dist (a,b) by METRIC_1:def_1;
hence  ( the distance of DF . (a,b) = 0 iff a = b ) by METRIC_1:1, METRIC_1:2; ::_thesis: (  the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
 the distance of DF . (b,a) = dist (b,a) by METRIC_1:def_1;
hence  the distance of DF . (a,b) = the distance of DF . (b,a) by A2; ::_thesis: the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c))
 ( the distance of DF . (a,c) = dist (a,c) & the distance of DF . (b,c) = dist (b,c) ) by METRIC_1:def_1;
hence  the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) by A2, METRIC_1:4; ::_thesis: verum
end;
hence  f is_metric_of D by Def6; ::_thesis: verum
end;
 ( f is_metric_of D implies MetrStruct(# D,f #) is MetrSpace )
proof
assume A3: f is_metric_of D ; ::_thesis: MetrStruct(# D,f #) is MetrSpace
 for a, b, c being Element of MetrStruct(# D,f #) holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
proof
let a, b, c be Element of MetrStruct(# D,f #); ::_thesis: ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A4: the distance of MetrStruct(# D,f #) . (a,b) = dist (a,b) by METRIC_1:def_1;
hence  ( dist (a,b) = 0 iff a = b ) by A3, Def6; ::_thesis: (  dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
 the distance of MetrStruct(# D,f #) . (b,a) = dist (b,a) by METRIC_1:def_1;
hence  dist (a,b) = dist (b,a) by A3, A4, Def6; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
 ( the distance of MetrStruct(# D,f #) . (a,c) = dist (a,c) & the distance of MetrStruct(# D,f #) . (b,c) = dist (b,c) ) by METRIC_1:def_1;
hence  dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A3, A4, Def6; ::_thesis: verum
end;
hence  MetrStruct(# D,f #) is MetrSpace by METRIC_1:6; ::_thesis: verum
end;
hence  ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace ) by A1; ::_thesis: verum
end;

definition
let D be set ;
let f be Function of [:D,D:],REAL;
assume A1: f is_metric_of D ;
func SpaceMetr (D,f) ->  strict MetrSpace equals :Def7: :: PCOMPS_1:def 7
 MetrStruct(# D,f #);
coherence
 MetrStruct(# D,f #) is strict MetrSpace by A1, Th35;
end;

:: deftheorem Def7 defines SpaceMetr PCOMPS_1:def_7_:_
 for D being set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
SpaceMetr (D,f) = MetrStruct(# D,f #);

definition
let IT be TopStruct ;
attrIT is metrizable  means :: PCOMPS_1:def 8
 ex f being Function of [: the carrier of IT, the carrier of IT:],REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr ( the carrier of IT,f)) = the topology of IT );
end;

:: deftheorem  defines metrizable PCOMPS_1:def_8_:_
 for IT being TopStruct holds
( IT is metrizable iff ex f being Function of [: the carrier of IT, the carrier of IT:],REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr ( the carrier of IT,f)) = the topology of IT ) );

registration
cluster non empty strict TopSpace-like metrizable for TopStruct ;
existence
 ex b1 being non empty TopSpace st
( b1 is strict & b1 is metrizable )
proof
set MS = the non empty strict MetrSpace;
take TS = TopSpaceMetr the non empty strict MetrSpace; ::_thesis: ( TS is strict & TS is metrizable )
reconsider f = the distance of the non empty strict MetrSpace as Function of [: the carrier of TS, the carrier of TS:],REAL ;
thus  TS is strict ; ::_thesis: TS is metrizable
take  f ; :: according to PCOMPS_1:def_8 ::_thesis: ( f is_metric_of the carrier of TS & Family_open_set (SpaceMetr ( the carrier of TS,f)) = the topology of TS )
thus  f is_metric_of the carrier of TS by Th35; ::_thesis: Family_open_set (SpaceMetr ( the carrier of TS,f)) = the topology of TS
hence  Family_open_set (SpaceMetr ( the carrier of TS,f)) = the topology of TS by Def7; ::_thesis: verum
end;
end;

theorem :: PCOMPS_1:36
for D being non empty set
for f being Function of [:D,D:],REAL st f is_metric_of D holds
not SpaceMetr (D,f) is empty
proof
let D be non empty set ; ::_thesis: for f being Function of [:D,D:],REAL st f is_metric_of D holds
not SpaceMetr (D,f) is empty
let f be Function of [:D,D:],REAL; ::_thesis: ( f is_metric_of D implies not SpaceMetr (D,f) is empty )
assume  f is_metric_of D ; ::_thesis: not SpaceMetr (D,f) is empty
then  SpaceMetr (D,f) = MetrStruct(# D,f #) by Def7;
hence  not SpaceMetr (D,f) is empty ; ::_thesis: verum
end;