for T being non empty TopSpace-like TopRelStr holds
( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T )