let T be connected TopSpace; :: thesis: for A being open closed Subset of T holds
( A = {} or A = [#] T )
let A be open closed Subset of T; :: thesis: ( A = {} or A = [#] T )
assume that
A1: A <> {} and
A2: A <> [#] T ; :: thesis: contradiction
A3: A ` <> {} by A2, PRE_TOPC:4;
A misses A ` by SUBSET_1:24;
then A4: A,A ` are_separated by CONNSP_1:2;
A5: [#] T = A \/ (A `) by PRE_TOPC:2;
A <> {} T by A1;
then not [#] T is connected by A5, A4, A3, CONNSP_1:15;
hence contradiction by CONNSP_1:27; :: thesis: verum