reconsider F = Family_open_set ET as Subset-Family of ET ;

let x be object ; :: according to TARSKI:def 3,FINTOPO7:def 13 :: thesis: ( not x in Family_open_set ET or x in UniCl (Family_open_set ET) )

assume A1: x in Family_open_set ET ; :: thesis: x in UniCl (Family_open_set ET)

then reconsider B = {x} as Subset-Family of ET by SUBSET_1:41;

A2: B c= Family_open_set ET by A1, ZFMISC_1:31;

x = union B ;

hence x in UniCl (Family_open_set ET) by A2, CANTOR_1:def 1; :: thesis: verum

let x be object ; :: according to TARSKI:def 3,FINTOPO7:def 13 :: thesis: ( not x in Family_open_set ET or x in UniCl (Family_open_set ET) )

assume A1: x in Family_open_set ET ; :: thesis: x in UniCl (Family_open_set ET)

then reconsider B = {x} as Subset-Family of ET by SUBSET_1:41;

A2: B c= Family_open_set ET by A1, ZFMISC_1:31;

x = union B ;

hence x in UniCl (Family_open_set ET) by A2, CANTOR_1:def 1; :: thesis: verum