A1: {X} c= bool X by ZFMISC_1:80;
Fin X c= bool X by FINSUB_1:26;
then reconsider F = {X} \/ (Fin X) as Subset-Family of X by A1, 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