( {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

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