set S = { A where A is Subset of (COMPLEX n) : A is open } ;
{ A where A is Subset of (COMPLEX n) : A is open } c= bool (COMPLEX n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of (COMPLEX n) : A is open } or x in bool (COMPLEX n) )
assume x in { A where A is Subset of (COMPLEX n) : A is open } ; :: thesis: x in bool (COMPLEX n)
then ex A being Subset of (COMPLEX n) st
( x = A & A is open ) ;
hence x in bool (COMPLEX n) ; :: thesis: verum

end;

hence { A where A is Subset of (COMPLEX n) : A is open } is Subset-Family of (COMPLEX n) ; :: thesis: verum