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

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