for X, Y being non emptyset for f being Function of X,Y for A being Subset of X st ( for x1, x2 being Element of X st x1 in A & f . x1 = f . x2 holds x2 in A ) holds f "(f .: A)= A
redefine attr T is T_0 means :Def7: :: T_0TOPSP:def 7 ( T is empty or for x, y being Point of T st x <> y holds ex V being Subset of T st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) );
compatibility
( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds ex V being Subset of T st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) )
:: deftheorem Def7 defines T_0T_0TOPSP:def 7 : for T being TopStruct holds ( T is T_0 iff ( T is empty or for x, y being Point of T st x <> y holds ex V being Subset of T st ( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) ) ) );
:: Preliminaries
::