take the topology of X ; :: according to CANTOR_1:def 4 :: 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