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