let T be TopSpace; :: thesis: the topology of T = UniCl the topology of T
thus the topology of T c= UniCl the topology of T by Th1; :: according to XBOOLE_0:def 10 :: thesis: UniCl the topology of T c= the topology of T
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in UniCl the topology of T or a in the topology of T )
assume A1: a in UniCl the topology of T ; :: thesis: a in the topology of T
then reconsider a9 = a as Subset of T ;
ex b being Subset-Family of T st
( b c= the topology of T & a9 = union b ) by A1, Def1;
hence a in the topology of T by PRE_TOPC:def 1; :: thesis: verum