( {X} c= bool X & Fin X c= bool X ) by FINSUB_1:13, ZFMISC_1:68;
then reconsider F = {X} \/ (Fin X) as Subset-Family of X by XBOOLE_1:8;
reconsider F = F as Subset-Family of X ;
take T = TopStruct(# X,(COMPLEMENT F) #); :: thesis: ( the carrier of T = X & COMPLEMENT the topology of T = {X} \/ (Fin X) )
thus the carrier of T = X ; :: thesis: COMPLEMENT the topology of T = {X} \/ (Fin X)
thus COMPLEMENT the topology of T = {X} \/ (Fin X) ; :: thesis: verum