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 <> {} T by A1;
A4: [#] T = A \/ (A ` ) by PRE_TOPC:18;
A misses A ` by SUBSET_1:44;
then A5: A,A ` are_separated by A4, CONNSP_1:3;
A ` <> {} by A2, PRE_TOPC:23;
then not [#] T is connected by A3, A4, A5, CONNSP_1:16;
hence contradiction by CONNSP_1:28; :: thesis: verum