{({} T)} c= bool the carrier of T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {({} T)} or x in bool the carrier of T )
assume x in {({} T)} ; :: thesis: x in bool the carrier of T
then x = {} T by TARSKI:def 1;
hence x in bool the carrier of T ; :: thesis: verum
end;
then reconsider F = {({} T)} as Subset-Family of T ;
take F ; :: thesis: ( not F is empty & F is open & F is closed & F is connected )
thus not F is empty ; :: thesis: ( F is open & F is closed & F is connected )
thus for P being Subset of T st P in F holds
P is open by TARSKI:def 1; :: according to TOPS_2:def 1 :: thesis: ( F is closed & F is connected )
thus for P being Subset of T st P in F holds
P is closed by TARSKI:def 1; :: according to TOPS_2:def 2 :: thesis: F is connected
thus for P being Subset of T st P in F holds
P is connected by TARSKI:def 1; :: according to RCOMP_3:def 1 :: thesis: verum