let T be non empty TopSpace; :: thesis: the topology of T = UniCl (FinMeetCl the topology of T)
the topology of T = FinMeetCl the topology of T by Th5;
hence the topology of T = UniCl (FinMeetCl the topology of T) by Th6; :: thesis: verum