reconsider E = {} as Subset-Family of T by Th18;
consider Y being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T such that
E c= Y and
A1: for Z being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T st E c= Z holds
Y c= Z by Th63;
take Y ; :: thesis: for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds Y c= G
let G be compl-closed all-open-containing closed_for_countable_unions Subset-Family of T; :: thesis: Y c= G
thus Y c= G by A1, XBOOLE_1:2; :: thesis: verum