set a = { O where O is open Subset of NT : O c= A } ;

now :: thesis: for o being object st o in { O where O is open Subset of NT : O c= A } holds
o in bool the carrier of NT

let o be object ; :: thesis: ( o in { O where O is open Subset of NT : O c= A } implies o in bool the carrier of NT )
assume o in { O where O is open Subset of NT : O c= A } ; :: thesis: o in bool the carrier of NT
then ex O being open Subset of NT st
( o = O & O c= A ) ;
hence o in bool the carrier of NT ; :: thesis: verum

end;

then { O where O is open Subset of NT : O c= A } c= bool the carrier of NT ;
then reconsider a = { O where O is open Subset of NT : O c= A } as Subset-Family of NT ;

now :: thesis: for o being object st o in a holds
o in Family_open_set NT

let o be object ; :: thesis: ( o in a implies o in Family_open_set NT )
assume o in a ; :: thesis: o in Family_open_set NT
then consider O being open Subset of NT such that
A1: o = O and
O c= A ;
O in { O where O is open Subset of NT : verum } ;
hence o in Family_open_set NT by A1, FINTOPO7:def 11; :: thesis: verum

end;

then a c= Family_open_set NT ;
then union a in Family_open_set NT by FINTOPO7:14;
then union a in { O where O is open Subset of NT : verum } by FINTOPO7:def 11;
then ex O being open Subset of NT st union a = O ;
hence Int A is open by Lm5; :: thesis: verum