take the topology of X ; :: according to CANTOR_1:def 5 :: thesis: the topology of X c= FinMeetCl the topology of X
thus the topology of X c= FinMeetCl the topology of X by Th4; :: thesis: verum