connsp_1.miz



    begin

    reserve GX for TopSpace;

    reserve A,B,C for Subset of GX;

    reserve TS for TopStruct;

    reserve K,K1,L,L1 for Subset of TS;

    definition

      let GX be TopStruct, A,B be Subset of GX;

      :: CONNSP_1:def1

      pred A,B are_separated means ( Cl A) misses B & A misses ( Cl B);

      symmetry ;

    end

    theorem :: CONNSP_1:1

    

     Th1: (K,L) are_separated implies K misses L

    proof

      assume that

       A1: (( Cl K) /\ L) = {} and (K /\ ( Cl L)) = {} ;

      K c= ( Cl K) by PRE_TOPC: 18;

      hence (K /\ L) = {} by A1, XBOOLE_1: 3, XBOOLE_1: 27;

    end;

    theorem :: CONNSP_1:2

    

     Th2: K is closed & L is closed & K misses L implies (K,L) are_separated by PRE_TOPC: 22;

    theorem :: CONNSP_1:3

    

     Th3: ( [#] GX) = (A \/ B) & A is open & B is open & A misses B implies (A,B) are_separated

    proof

      assume that

       A1: ( [#] GX) = (A \/ B) and

       A2: A is open and

       A3: B is open and

       A4: A misses B;

      

       A5: ( Cl (( [#] GX) \ B)) = (( [#] GX) \ B) by A3, PRE_TOPC: 23;

      A = (( [#] GX) \ B) by A1, A4, PRE_TOPC: 5;

      then

       A6: A is closed by A5, PRE_TOPC: 22;

      

       A7: ( Cl (( [#] GX) \ A)) = (( [#] GX) \ A) by A2, PRE_TOPC: 23;

      B = (( [#] GX) \ A) by A1, A4, PRE_TOPC: 5;

      then B is closed by A7, PRE_TOPC: 22;

      hence thesis by A4, A6, Th2;

    end;

    theorem :: CONNSP_1:4

    

     Th4: ( [#] GX) = (A \/ B) & (A,B) are_separated implies A is open closed & B is open closed

    proof

      assume that

       A1: ( [#] GX) = (A \/ B) and

       A2: (A,B) are_separated ;

      

       A3: (( [#] GX) \ B) = A by A1, A2, Th1, PRE_TOPC: 5;

      B c= ( Cl B) by PRE_TOPC: 18;

      then

       A4: A misses ( Cl B) implies ( Cl B) = B by A1, XBOOLE_1: 73;

      A c= ( Cl A) by PRE_TOPC: 18;

      then

       A5: ( Cl A) misses B implies ( Cl A) = A by A1, XBOOLE_1: 73;

      B = (( [#] GX) \ A) by A1, A2, Th1, PRE_TOPC: 5;

      hence thesis by A2, A5, A4, A3, PRE_TOPC: 22, PRE_TOPC: 23;

    end;

    theorem :: CONNSP_1:5

    

     Th5: for X9 be SubSpace of GX, P1,Q1 be Subset of GX, P,Q be Subset of X9 st P = P1 & Q = Q1 holds (P,Q) are_separated implies (P1,Q1) are_separated

    proof

      let X9 be SubSpace of GX, P1,Q1 be Subset of GX, P,Q be Subset of X9 such that

       A1: P = P1 and

       A2: Q = Q1;

      reconsider P2 = P, Q2 = Q as Subset of GX by PRE_TOPC: 11;

      assume that

       A3: (( Cl P) /\ Q) = {} and

       A4: (P /\ ( Cl Q)) = {} ;

      (P /\ ( Cl Q)) = (P /\ (( [#] X9) /\ ( Cl Q2))) by PRE_TOPC: 17

      .= ((P /\ ( [#] X9)) /\ ( Cl Q2)) by XBOOLE_1: 16

      .= (P2 /\ ( Cl Q2)) by XBOOLE_1: 28;

      then

       A5: P2 misses ( Cl Q2) by A4;

      (( Cl P) /\ Q) = ((( Cl P2) /\ ( [#] X9)) /\ Q) by PRE_TOPC: 17

      .= (( Cl P2) /\ (Q /\ ( [#] X9))) by XBOOLE_1: 16

      .= (( Cl P2) /\ Q2) by XBOOLE_1: 28;

      then ( Cl P2) misses Q2 by A3;

      hence thesis by A1, A2, A5;

    end;

    theorem :: CONNSP_1:6

    

     Th6: for X9 be SubSpace of GX, P,Q be Subset of GX, P1,Q1 be Subset of X9 st P = P1 & Q = Q1 & (P \/ Q) c= ( [#] X9) holds (P,Q) are_separated implies (P1,Q1) are_separated

    proof

      let X9 be SubSpace of GX, P,Q be Subset of GX, P1,Q1 be Subset of X9 such that

       A1: P = P1 and

       A2: Q = Q1 and

       A3: (P \/ Q) c= ( [#] X9);

      

       A4: Q c= (P \/ Q) by XBOOLE_1: 7;

      P c= (P \/ Q) by XBOOLE_1: 7;

      then

      reconsider P2 = P, Q2 = Q as Subset of X9 by A3, A4, XBOOLE_1: 1;

      assume that

       A5: (( Cl P) /\ Q) = {} and

       A6: (P /\ ( Cl Q)) = {} ;

      (P2 /\ ( Cl Q2)) = (P2 /\ (( [#] X9) /\ ( Cl Q))) by PRE_TOPC: 17

      .= ((P2 /\ ( [#] X9)) /\ ( Cl Q)) by XBOOLE_1: 16

      .= (P /\ ( Cl Q)) by XBOOLE_1: 28;

      then

       A7: P2 misses ( Cl Q2) by A6;

      ( Cl P2) = (( Cl P) /\ ( [#] X9)) by PRE_TOPC: 17;

      

      then (( Cl P2) /\ Q2) = (( Cl P) /\ (Q2 /\ ( [#] X9))) by XBOOLE_1: 16

      .= (( Cl P) /\ Q) by XBOOLE_1: 28;

      then ( Cl P2) misses Q2 by A5;

      hence thesis by A1, A2, A7;

    end;

    theorem :: CONNSP_1:7

    

     Th7: (K,L) are_separated & K1 c= K & L1 c= L implies (K1,L1) are_separated

    proof

      assume that

       A1: (( Cl K) /\ L) = {} and

       A2: (K /\ ( Cl L)) = {} and

       A3: K1 c= K and

       A4: L1 c= L;

      ( Cl L1) c= ( Cl L) by A4, PRE_TOPC: 19;

      then (K1 /\ ( Cl L1)) = ( {} TS) by A2, A3, XBOOLE_1: 3, XBOOLE_1: 27;

      then

       A5: K1 misses ( Cl L1);

      ( Cl K1) c= ( Cl K) by A3, PRE_TOPC: 19;

      then (( Cl K1) /\ L1) = ( {} TS) by A1, A4, XBOOLE_1: 3, XBOOLE_1: 27;

      then ( Cl K1) misses L1;

      hence thesis by A5;

    end;

    theorem :: CONNSP_1:8

    

     Th8: (A,B) are_separated & (A,C) are_separated implies (A,(B \/ C)) are_separated

    proof

      assume that

       A1: ( Cl A) misses B and

       A2: A misses ( Cl B) and

       A3: ( Cl A) misses C and

       A4: A misses ( Cl C);

      

       A5: (A /\ ( Cl B)) = {} by A2;

      (A /\ ( Cl (B \/ C))) = (A /\ (( Cl B) \/ ( Cl C))) by PRE_TOPC: 20

      .= ((A /\ ( Cl B)) \/ (A /\ ( Cl C))) by XBOOLE_1: 23

      .= ( {} GX) by A4, A5;

      then

       A6: A misses ( Cl (B \/ C));

      

       A7: (( Cl A) /\ B) = {} by A1;

      (( Cl A) /\ (B \/ C)) = ((( Cl A) /\ B) \/ (( Cl A) /\ C)) by XBOOLE_1: 23

      .= ( {} GX) by A3, A7;

      then ( Cl A) misses (B \/ C);

      hence thesis by A6;

    end;

    theorem :: CONNSP_1:9

    

     Th9: K is closed & L is closed or K is open & L is open implies ((K \ L),(L \ K)) are_separated

    proof

       A1:

      now

        let K,L be Subset of TS such that

         A2: K is open and

         A3: L is open;

        

         A4: (K /\ (L ` )) c= K by XBOOLE_1: 17;

        

         A5: (( Cl L) /\ (K ` )) c= (K ` ) by XBOOLE_1: 17;

        ( Cl (( [#] TS) \ K)) = (( [#] TS) \ K) by A2, PRE_TOPC: 23;

        then

         A6: ((K /\ (L ` )) /\ (( Cl L) /\ ( Cl (K ` )))) c= (K /\ (K ` )) by A4, A5, XBOOLE_1: 27;

        

         A7: (K \ L) = (K /\ (L ` )) by SUBSET_1: 13;

        

         A8: (L /\ (K ` )) c= L by XBOOLE_1: 17;

        (( Cl K) /\ (L ` )) c= (L ` ) by XBOOLE_1: 17;

        then

         A9: ((( Cl K) /\ (L ` )) /\ (L /\ (K ` ))) c= (L /\ (L ` )) by A8, XBOOLE_1: 27;

        L misses (L ` ) by XBOOLE_1: 79;

        then

         A10: (L /\ (L ` )) = {} ;

        K misses (K ` ) by XBOOLE_1: 79;

        then

         A11: (K /\ (K ` )) = {} ;

        (( [#] TS) \ K) = (K ` );

        then

         A12: ((( Cl K) /\ ( Cl (L ` ))) /\ (L /\ (K ` ))) = ((( Cl K) /\ (L ` )) /\ (L /\ (K ` ))) by A3, PRE_TOPC: 23;

        

         A13: (L \ K) = (L /\ (K ` )) by SUBSET_1: 13;

        ( Cl (L /\ (K ` ))) c= (( Cl L) /\ ( Cl (K ` ))) by PRE_TOPC: 21;

        then ((K \ L) /\ ( Cl (L \ K))) c= ((K /\ (L ` )) /\ (( Cl L) /\ ( Cl (K ` )))) by A7, A13, XBOOLE_1: 27;

        then ((K \ L) /\ ( Cl (L \ K))) = ( {} TS) by A11, A6;

        then

         A14: (K \ L) misses ( Cl (L \ K));

        ( Cl (K /\ (L ` ))) c= (( Cl K) /\ ( Cl (L ` ))) by PRE_TOPC: 21;

        then (( Cl (K \ L)) /\ (L \ K)) c= ((( Cl K) /\ ( Cl (L ` ))) /\ (L /\ (K ` ))) by A7, A13, XBOOLE_1: 27;

        then (( Cl (K \ L)) /\ (L \ K)) = ( {} TS) by A12, A10, A9;

        then ( Cl (K \ L)) misses (L \ K);

        hence ((K \ L),(L \ K)) are_separated by A14;

      end;

       A15:

      now

        let K,L be Subset of TS;

        assume that

         A16: K is closed and

         A17: L is closed;

        

         A18: (( [#] TS) \ L) is open by A17, PRE_TOPC:def 3;

        

         A19: ((( [#] TS) \ K) \ (( [#] TS) \ L)) = ((K ` ) /\ ((( [#] TS) \ L) ` )) by SUBSET_1: 13

        .= ((K ` ) /\ L) by PRE_TOPC: 3

        .= (L \ K) by SUBSET_1: 13;

        

         A20: ((( [#] TS) \ L) \ (( [#] TS) \ K)) = ((L ` ) /\ ((( [#] TS) \ K) ` )) by SUBSET_1: 13

        .= ((L ` ) /\ K) by PRE_TOPC: 3

        .= (K \ L) by SUBSET_1: 13;

        (( [#] TS) \ K) is open by A16, PRE_TOPC:def 3;

        hence ((K \ L),(L \ K)) are_separated by A1, A18, A20, A19;

      end;

      assume K is closed & L is closed or K is open & L is open;

      hence thesis by A1, A15;

    end;

    definition

      let GX be TopStruct;

      :: CONNSP_1:def2

      attr GX is connected means for A,B be Subset of GX st ( [#] GX) = (A \/ B) & (A,B) are_separated holds A = ( {} GX) or B = ( {} GX);

    end

    theorem :: CONNSP_1:10

    

     Th10: GX is connected iff for A,B be Subset of GX st ( [#] GX) = (A \/ B) & A <> ( {} GX) & B <> ( {} GX) & A is closed & B is closed holds A meets B

    proof

       A1:

      now

        assume not GX is connected;

        then

        consider P,Q be Subset of GX such that

         A2: ( [#] GX) = (P \/ Q) and

         A3: (P,Q) are_separated and

         A4: P <> ( {} GX) and

         A5: Q <> ( {} GX);

        

         A6: Q is closed by A2, A3, Th4;

        P is closed by A2, A3, Th4;

        hence ex A,B be Subset of GX st ( [#] GX) = (A \/ B) & A <> ( {} GX) & B <> ( {} GX) & A is closed & B is closed & A misses B by A2, A3, A4, A5, A6, Th1;

      end;

      (ex A,B be Subset of GX st ( [#] GX) = (A \/ B) & A <> ( {} GX) & B <> ( {} GX) & A is closed & B is closed & A misses B) implies not GX is connected by Th2;

      hence thesis by A1;

    end;

    theorem :: CONNSP_1:11

    GX is connected iff for A,B be Subset of GX st ( [#] GX) = (A \/ B) & A <> ( {} GX) & B <> ( {} GX) & A is open & B is open holds A meets B

    proof

       A1:

      now

        assume not GX is connected;

        then

        consider P,Q be Subset of GX such that

         A2: ( [#] GX) = (P \/ Q) and

         A3: (P,Q) are_separated and

         A4: P <> ( {} GX) and

         A5: Q <> ( {} GX);

        reconsider P, Q as Subset of GX;

        

         A6: Q is open by A2, A3, Th4;

        P is open by A2, A3, Th4;

        hence ex A,B be Subset of GX st ( [#] GX) = (A \/ B) & A <> ( {} GX) & B <> ( {} GX) & A is open & B is open & A misses B by A2, A3, A4, A5, A6, Th1;

      end;

      (ex A,B be Subset of GX st ( [#] GX) = (A \/ B) & A <> ( {} GX) & B <> ( {} GX) & A is open & B is open & A misses B) implies not GX is connected by Th3;

      hence thesis by A1;

    end;

    theorem :: CONNSP_1:12

    

     Th12: GX is connected iff for A be Subset of GX st A <> ( {} GX) & A <> ( [#] GX) holds ( Cl A) meets ( Cl (( [#] GX) \ A))

    proof

       A1:

      now

        given A be Subset of GX such that

         A2: A <> ( {} GX) and

         A3: A <> ( [#] GX) and

         A4: ( Cl A) misses ( Cl (( [#] GX) \ A));

        

         A5: (( Cl A) /\ ( Cl (( [#] GX) \ A))) = {} by A4;

        A c= ( Cl A) by PRE_TOPC: 18;

        then (A /\ ( Cl (( [#] GX) \ A))) = ( {} GX) by A5, XBOOLE_1: 3, XBOOLE_1: 27;

        then

         A6: A misses ( Cl (( [#] GX) \ A));

        

         A7: ( [#] GX) = (A \/ (A ` )) by PRE_TOPC: 2;

        

         A8: (( [#] GX) \ A) <> ( {} GX) by A3, PRE_TOPC: 4;

        (( [#] GX) \ A) c= ( Cl (( [#] GX) \ A)) by PRE_TOPC: 18;

        then (( Cl A) /\ (( [#] GX) \ A)) = {} by A5, XBOOLE_1: 3, XBOOLE_1: 27;

        then ( Cl A) misses (( [#] GX) \ A);

        then (A,(( [#] GX) \ A)) are_separated by A6;

        hence not GX is connected by A2, A8, A7;

      end;

      now

        assume not GX is connected;

        then

        consider A,B be Subset of GX such that

         A9: ( [#] GX) = (A \/ B) and

         A10: A <> ( {} GX) and

         A11: B <> ( {} GX) and

         A12: A is closed and

         A13: B is closed and

         A14: A misses B by Th10;

        

         A15: ( Cl A) = A by A12, PRE_TOPC: 22;

        

         A16: ( Cl B) = B by A13, PRE_TOPC: 22;

        

         A17: B = (( [#] GX) \ A) by A9, A14, PRE_TOPC: 5;

        then A <> ( [#] GX) by A11, PRE_TOPC: 4;

        hence ex A be Subset of GX st A <> ( {} GX) & A <> ( [#] GX) & ( Cl A) misses ( Cl (( [#] GX) \ A)) by A10, A14, A17, A15, A16;

      end;

      hence thesis by A1;

    end;

    theorem :: CONNSP_1:13

    GX is connected iff for A be Subset of GX st A is open closed holds A = ( {} GX) or A = ( [#] GX)

    proof

       A1:

      now

        assume not GX is connected;

        then

        consider P,Q be Subset of GX such that

         A2: ( [#] GX) = (P \/ Q) and

         A3: (P,Q) are_separated and

         A4: P <> ( {} GX) and

         A5: Q <> ( {} GX);

        reconsider P, Q as Subset of GX;

        Q = (( [#] GX) \ P) by A2, A3, Th1, PRE_TOPC: 5;

        then

         A6: P <> ( [#] GX) by A5, PRE_TOPC: 4;

        P is open closed by A2, A3, Th4;

        hence ex P be Subset of GX st P is open closed & P <> ( {} GX) & P <> ( [#] GX) by A4, A6;

      end;

      now

        given A1 be Subset of GX such that

         A7: A1 is open closed and

         A8: A1 <> ( {} GX) and

         A9: A1 <> ( [#] GX);

        

         A10: ( Cl (( [#] GX) \ A1)) = (( [#] GX) \ A1) by A7, PRE_TOPC: 23;

        

         A11: A1 misses (A1 ` ) by XBOOLE_1: 79;

        ( Cl A1) = A1 by A7, PRE_TOPC: 22;

        hence not GX is connected by A8, A9, A10, A11, Th12;

      end;

      hence thesis by A1;

    end;

    theorem :: CONNSP_1:14

    for GY be TopSpace holds for F be Function of GX, GY st F is continuous & (F .: ( [#] GX)) = ( [#] GY) & GX is connected holds GY is connected

    proof

      let GY be TopSpace;

      let F be Function of GX, GY such that

       A1: F is continuous and

       A2: (F .: ( [#] GX)) = ( [#] GY) and

       A3: GX is connected;

      assume not GY is connected;

      then

      consider A,B be Subset of GY such that

       A4: ( [#] GY) = (A \/ B) and

       A5: A <> ( {} GY) and

       A6: B <> ( {} GY) and

       A7: A is closed and

       A8: B is closed and

       A9: A misses B by Th10;

      

       A10: (F " A) is closed by A1, A7, PRE_TOPC:def 6;

      

       A11: (F " B) is closed by A1, A8, PRE_TOPC:def 6;

      

       A12: (A /\ B) = {} by A9;

      ((F " A) /\ (F " B)) = (F " (A /\ B)) by FUNCT_1: 68

      .= {} by A12;

      then

       A13: (F " A) misses (F " B);

      the carrier of GY is non empty by A5;

      

      then

       A14: ( [#] GX) = (F " the carrier of GY) by FUNCT_2: 40

      .= ((F " A) \/ (F " B)) by A4, RELAT_1: 140;

      

       A15: ( rng F) = (F .: the carrier of GX) by RELSET_1: 22;

      then

       A16: (F " B) <> ( {} GX) by A2, A6, RELAT_1: 139;

      (F " A) <> ( {} GX) by A2, A5, A15, RELAT_1: 139;

      hence contradiction by A3, A14, A13, A10, A11, A16, Th10;

    end;

    definition

      let GX be TopStruct, A be Subset of GX;

      :: CONNSP_1:def3

      attr A is connected means

      : Def3: (GX | A) is connected;

    end

    theorem :: CONNSP_1:15

    

     Th15: A is connected iff for P,Q be Subset of GX st A = (P \/ Q) & (P,Q) are_separated holds P = ( {} GX) or Q = ( {} GX)

    proof

      

       A1: ( [#] (GX | A)) = A by PRE_TOPC:def 5;

       A2:

      now

        assume not A is connected;

        then not (GX | A) is connected;

        then

        consider P,Q be Subset of (GX | A) such that

         A3: ( [#] (GX | A)) = (P \/ Q) and

         A4: (P,Q) are_separated and

         A5: P <> ( {} (GX | A)) and

         A6: Q <> ( {} (GX | A));

        reconsider Q1 = Q as Subset of GX by PRE_TOPC: 11;

        reconsider P1 = P as Subset of GX by PRE_TOPC: 11;

        (P1,Q1) are_separated by A4, Th5;

        hence ex P1,Q1 be Subset of GX st A = (P1 \/ Q1) & (P1,Q1) are_separated & P1 <> ( {} GX) & Q1 <> ( {} GX) by A1, A3, A5, A6;

      end;

      now

        given P,Q be Subset of GX such that

         A7: A = (P \/ Q) and

         A8: (P,Q) are_separated and

         A9: P <> ( {} GX) and

         A10: Q <> ( {} GX);

        reconsider Q1 = Q as Subset of (GX | A) by A1, A7, XBOOLE_1: 7;

        reconsider P1 = P as Subset of (GX | A) by A1, A7, XBOOLE_1: 7;

        (P1,Q1) are_separated by A1, A7, A8, Th6;

        then not (GX | A) is connected by A1, A7, A9, A10;

        hence not A is connected;

      end;

      hence thesis by A2;

    end;

    theorem :: CONNSP_1:16

    

     Th16: A is connected & A c= (B \/ C) & (B,C) are_separated implies A c= B or A c= C

    proof

      assume that

       A1: A is connected and

       A2: A c= (B \/ C) and

       A3: (B,C) are_separated ;

      

       A4: (A /\ C) c= C by XBOOLE_1: 17;

      (A /\ B) c= B by XBOOLE_1: 17;

      then

       A5: ((A /\ B),(A /\ C)) are_separated by A3, A4, Th7;

      

       A6: ((A /\ B) \/ (A /\ C)) = (A /\ (B \/ C)) by XBOOLE_1: 23

      .= A by A2, XBOOLE_1: 28;

      assume that

       A7: not A c= B and

       A8: not A c= C;

      A meets C by A2, A7, XBOOLE_1: 73;

      then

       A9: (A /\ C) <> {} ;

      A meets B by A2, A8, XBOOLE_1: 73;

      then

       A10: (A /\ B) <> {} ;

      then A <> ( {} GX);

      hence contradiction by A1, A10, A9, A5, A6, Th15;

    end;

    theorem :: CONNSP_1:17

    

     Th17: A is connected & B is connected & not (A,B) are_separated implies (A \/ B) is connected

    proof

      assume that

       A1: A is connected and

       A2: B is connected and

       A3: not (A,B) are_separated ;

      assume not (A \/ B) is connected;

      then

      consider P,Q be Subset of GX such that

       A4: (A \/ B) = (P \/ Q) and

       A5: (P,Q) are_separated and

       A6: P <> ( {} GX) and

       A7: Q <> ( {} GX) by Th15;

      

       A8: not (A c= Q & B c= P) by A3, A5, Th7;

      P misses Q by A5, Th1;

      then

       A9: (P /\ Q) = {} ;

       A10:

      now

        

         A11: P c= (P \/ Q) by XBOOLE_1: 7;

        assume that

         A12: A c= P and

         A13: B c= P;

        (A \/ B) c= P by A12, A13, XBOOLE_1: 8;

        then (P \/ Q) = P by A4, A11;

        hence contradiction by A7, A9, XBOOLE_1: 7, XBOOLE_1: 28;

      end;

       A14:

      now

        

         A15: Q c= (Q \/ P) by XBOOLE_1: 7;

        assume that

         A16: A c= Q and

         A17: B c= Q;

        (A \/ B) c= Q by A16, A17, XBOOLE_1: 8;

        then (Q \/ P) = Q by A4, A15;

        hence contradiction by A6, A9, XBOOLE_1: 7, XBOOLE_1: 28;

      end;

       not (A c= P & B c= Q) by A3, A5, Th7;

      hence contradiction by A1, A2, A4, A5, A10, A8, A14, Th16, XBOOLE_1: 7;

    end;

    theorem :: CONNSP_1:18

    

     Th18: C is connected & C c= A & A c= ( Cl C) implies A is connected

    proof

      assume that

       A1: C is connected and

       A2: C c= A and

       A3: A c= ( Cl C);

      assume not A is connected;

      then

      consider P,Q be Subset of GX such that

       A4: A = (P \/ Q) and

       A5: (P,Q) are_separated and

       A6: P <> ( {} GX) and

       A7: Q <> ( {} GX) by Th15;

      P misses ( Cl Q) by A5;

      then

       A8: (P /\ ( Cl Q)) = {} ;

       A9:

      now

        assume C c= Q;

        then ( Cl C) c= ( Cl Q) by PRE_TOPC: 19;

        then (P /\ ( Cl C)) = {} by A8, XBOOLE_1: 3, XBOOLE_1: 27;

        then (P /\ A) = {} by A3, XBOOLE_1: 3, XBOOLE_1: 27;

        hence contradiction by A4, A6, XBOOLE_1: 21;

      end;

      ( Cl P) misses Q by A5;

      then

       A10: (( Cl P) /\ Q) = {} ;

      now

        assume C c= P;

        then ( Cl C) c= ( Cl P) by PRE_TOPC: 19;

        then (( Cl C) /\ Q) = {} by A10, XBOOLE_1: 3, XBOOLE_1: 27;

        then (A /\ Q) = {} by A3, XBOOLE_1: 3, XBOOLE_1: 27;

        hence contradiction by A4, A7, XBOOLE_1: 21;

      end;

      hence contradiction by A1, A2, A4, A5, A9, Th16;

    end;

    theorem :: CONNSP_1:19

    

     Th19: A is connected implies ( Cl A) is connected

    proof

      

       A1: A c= ( Cl A) by PRE_TOPC: 18;

      assume A is connected;

      hence thesis by A1, Th18;

    end;

    theorem :: CONNSP_1:20

    

     Th20: GX is connected & A is connected & (( [#] GX) \ A) = (B \/ C) & (B,C) are_separated implies (A \/ B) is connected & (A \/ C) is connected

    proof

      assume that

       A1: GX is connected and

       A2: A is connected and

       A3: (( [#] GX) \ A) = (B \/ C) and

       A4: (B,C) are_separated ;

      now

        let A,B,C be Subset of GX such that

         A5: GX is connected and

         A6: A is connected and

         A7: (( [#] GX) \ A) = (B \/ C) and

         A8: (B,C) are_separated ;

        now

          let P,Q be Subset of GX such that

           A9: (A \/ B) = (P \/ Q) and

           A10: (P,Q) are_separated ;

          

           A11: ( [#] GX) = (A \/ (B \/ C)) by A7, XBOOLE_1: 45

          .= ((P \/ Q) \/ C) by A9, XBOOLE_1: 4;

           A12:

          now

            assume A c= Q;

            then P misses A by A10, Th1, Th7;

            then P c= B by A9, XBOOLE_1: 7, XBOOLE_1: 73;

            then (P,C) are_separated by A8, Th7;

            then

             A13: (P,(Q \/ C)) are_separated by A10, Th8;

            ( [#] GX) = (P \/ (Q \/ C)) by A11, XBOOLE_1: 4;

            hence P = ( {} GX) or Q = ( {} GX) by A5, A13;

          end;

          now

            assume A c= P;

            then Q misses A by A10, Th1, Th7;

            then Q c= B by A9, XBOOLE_1: 7, XBOOLE_1: 73;

            then (Q,C) are_separated by A8, Th7;

            then

             A14: (Q,(P \/ C)) are_separated by A10, Th8;

            ( [#] GX) = (Q \/ (P \/ C)) by A11, XBOOLE_1: 4;

            hence P = ( {} GX) or Q = ( {} GX) by A5, A14;

          end;

          hence P = ( {} GX) or Q = ( {} GX) by A6, A9, A10, A12, Th16, XBOOLE_1: 7;

        end;

        hence (A \/ B) is connected by Th15;

      end;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: CONNSP_1:21

    (( [#] GX) \ A) = (B \/ C) & (B,C) are_separated & A is closed implies (A \/ B) is closed & (A \/ C) is closed

    proof

      assume that

       A1: (( [#] GX) \ A) = (B \/ C) and

       A2: (B,C) are_separated and

       A3: A is closed;

      now

        let A,B,C be Subset of GX;

        assume that

         A4: (( [#] GX) \ A) = (B \/ C) and

         A5: (B,C) are_separated and

         A6: A is closed;

        

         A7: ( Cl A) = A by A6, PRE_TOPC: 22;

        ( Cl B) misses C by A5;

        then

         A8: (( Cl B) /\ C) = {} ;

        

         A9: ( [#] GX) = (A \/ (B \/ C)) by A4, XBOOLE_1: 45;

        ( Cl (A \/ B)) = (( Cl A) \/ ( Cl B)) by PRE_TOPC: 20

        .= (A \/ (( Cl B) /\ (A \/ (B \/ C)))) by A7, A9, XBOOLE_1: 28

        .= ((A \/ ( Cl B)) /\ (A \/ (A \/ (B \/ C)))) by XBOOLE_1: 24

        .= ((A \/ ( Cl B)) /\ ((A \/ A) \/ (B \/ C))) by XBOOLE_1: 4

        .= (A \/ (( Cl B) /\ (B \/ C))) by XBOOLE_1: 24

        .= (A \/ ((( Cl B) /\ B) \/ (( Cl B) /\ C))) by XBOOLE_1: 23

        .= (A \/ B) by A8, PRE_TOPC: 18, XBOOLE_1: 28;

        hence (A \/ B) is closed by PRE_TOPC: 22;

      end;

      hence thesis by A1, A2, A3;

    end;

    theorem :: CONNSP_1:22

    C is connected & C meets A & (C \ A) <> ( {} GX) implies C meets ( Fr A)

    proof

      assume that

       A1: C is connected and

       A2: C meets A and

       A3: (C \ A) <> ( {} GX);

      

       A4: (A ` ) c= ( Cl (A ` )) by PRE_TOPC: 18;

      ( Cl (C /\ A)) c= ( Cl A) by PRE_TOPC: 19, XBOOLE_1: 17;

      then

       A5: (( Cl (C /\ A)) /\ (A ` )) c= (( Cl A) /\ ( Cl (A ` ))) by A4, XBOOLE_1: 27;

      

       A6: A c= ( Cl A) by PRE_TOPC: 18;

      

       A7: (C \ A) = (C /\ (A ` )) by SUBSET_1: 13;

      then ( Cl (C \ A)) c= ( Cl (A ` )) by PRE_TOPC: 19, XBOOLE_1: 17;

      then (A /\ ( Cl (C /\ (A ` )))) c= (( Cl A) /\ ( Cl (A ` ))) by A7, A6, XBOOLE_1: 27;

      then ((( Cl (C /\ A)) /\ (A ` )) \/ (A /\ ( Cl (C /\ (A ` ))))) c= (( Cl A) /\ ( Cl (A ` ))) by A5, XBOOLE_1: 8;

      then

       A8: (C /\ ((( Cl (C /\ A)) /\ (A ` )) \/ (A /\ ( Cl (C /\ (A ` )))))) c= (C /\ (( Cl A) /\ ( Cl (A ` )))) by XBOOLE_1: 27;

      

       A9: C = (C /\ ( [#] GX)) by XBOOLE_1: 28

      .= (C /\ (A \/ (A ` ))) by PRE_TOPC: 2

      .= ((C /\ A) \/ (C \ A)) by A7, XBOOLE_1: 23;

      (C /\ A) <> {} by A2;

      then not ((C /\ A),(C \ A)) are_separated by A1, A3, A9, Th15;

      then ( Cl (C /\ A)) meets (C \ A) or (C /\ A) meets ( Cl (C \ A));

      then

       A10: (( Cl (C /\ A)) /\ (C \ A)) <> {} or ((C /\ A) /\ ( Cl (C \ A))) <> {} ;

      ((( Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ ( Cl (C \ A)))) = (((( Cl (C /\ A)) /\ C) /\ (A ` )) \/ ((C /\ A) /\ ( Cl (C /\ (A ` ))))) by A7, XBOOLE_1: 16

      .= (((C /\ ( Cl (C /\ A))) /\ (A ` )) \/ (C /\ (A /\ ( Cl (C /\ (A ` )))))) by XBOOLE_1: 16

      .= ((C /\ (( Cl (C /\ A)) /\ (A ` ))) \/ (C /\ (A /\ ( Cl (C /\ (A ` )))))) by XBOOLE_1: 16

      .= (C /\ ((( Cl (C /\ A)) /\ (A ` )) \/ (A /\ ( Cl (C /\ (A ` )))))) by XBOOLE_1: 23;

      then ((( Cl (C /\ A)) /\ (C \ A)) \/ ((C /\ A) /\ ( Cl (C \ A)))) c= (C /\ ( Fr A)) by A8, TOPS_1:def 2;

      hence (C /\ ( Fr A)) <> {} by A10;

    end;

    theorem :: CONNSP_1:23

    

     Th23: for X9 be SubSpace of GX, A be Subset of GX, B be Subset of X9 st A = B holds A is connected iff B is connected

    proof

      let X9 be SubSpace of GX, A be Subset of GX, B be Subset of X9;

      assume

       A1: A = B;

      reconsider GX9 = GX, X = X9 as TopSpace;

      

       A2: ( [#] (GX | A)) = A by PRE_TOPC:def 5;

      reconsider B9 = B as Subset of X;

      reconsider A9 = A as Subset of GX9;

      

       A3: ( [#] (X9 | B)) = B by PRE_TOPC:def 5;

       A4:

      now

        assume not A is connected;

        then not (GX9 | A9) is connected;

        then

        consider P,Q be Subset of (GX | A) such that

         A5: ( [#] (GX | A)) = (P \/ Q) and

         A6: P <> ( {} (GX | A)) and

         A7: Q <> ( {} (GX | A)) and

         A8: P is closed and

         A9: Q is closed and

         A10: P misses Q by Th10;

        consider P1 be Subset of GX such that

         A11: P1 is closed and

         A12: (P1 /\ ( [#] (GX | A))) = P by A8, PRE_TOPC: 13;

        reconsider P11 = (P1 /\ ( [#] X9)) as Subset of X9;

        

         A13: P11 is closed by A11, PRE_TOPC: 13;

        reconsider PP = P, QQ = Q as Subset of (X9 | B) by A1, A2, A3;

        

         A14: P c= ( [#] X9) by A1, A2, XBOOLE_1: 1;

        (P1 /\ A) c= P1 by XBOOLE_1: 17;

        then P c= (P1 /\ ( [#] X9)) by A2, A12, A14, XBOOLE_1: 19;

        then

         A15: P c= ((P1 /\ ( [#] X9)) /\ A) by A2, XBOOLE_1: 19;

        (P1 /\ ( [#] X9)) c= P1 by XBOOLE_1: 17;

        then ((P1 /\ ( [#] X9)) /\ A) c= P by A2, A12, XBOOLE_1: 27;

        then (P11 /\ ( [#] (X9 | B))) = PP by A1, A3, A15;

        then

         A16: PP is closed by A13, PRE_TOPC: 13;

        consider Q1 be Subset of GX such that

         A17: Q1 is closed and

         A18: (Q1 /\ ( [#] (GX | A))) = Q by A9, PRE_TOPC: 13;

        reconsider Q11 = (Q1 /\ ( [#] X9)) as Subset of X9;

        

         A19: Q c= ( [#] X9) by A1, A2, XBOOLE_1: 1;

        (Q1 /\ A) c= Q1 by XBOOLE_1: 17;

        then Q c= (Q1 /\ ( [#] X9)) by A2, A18, A19, XBOOLE_1: 19;

        then

         A20: Q c= ((Q1 /\ ( [#] X9)) /\ A) by A2, XBOOLE_1: 19;

        (Q1 /\ ( [#] X9)) c= Q1 by XBOOLE_1: 17;

        then ((Q1 /\ ( [#] X9)) /\ A) c= Q by A2, A18, XBOOLE_1: 27;

        then

         A21: ((Q1 /\ ( [#] X9)) /\ A) = Q by A20;

        Q11 is closed by A17, PRE_TOPC: 13;

        then QQ is closed by A1, A3, A21, PRE_TOPC: 13;

        then not (X | B9) is connected by A1, A2, A3, A5, A6, A7, A10, A16, Th10;

        hence not B is connected;

      end;

      now

        assume not B is connected;

        then not (X9 | B) is connected;

        then

        consider P,Q be Subset of (X9 | B) such that

         A22: ( [#] (X9 | B)) = (P \/ Q) and

         A23: P <> ( {} (X9 | B)) and

         A24: Q <> ( {} (X9 | B)) and

         A25: P is closed and

         A26: Q is closed and

         A27: P misses Q by Th10;

        reconsider QQ = Q as Subset of (GX | A) by A1, A2, A3;

        reconsider PP = P as Subset of (GX | A) by A1, A2, A3;

        consider P1 be Subset of X9 such that

         A28: P1 is closed and

         A29: (P1 /\ ( [#] (X9 | B))) = P by A25, PRE_TOPC: 13;

        consider Q1 be Subset of X9 such that

         A30: Q1 is closed and

         A31: (Q1 /\ ( [#] (X9 | B))) = Q by A26, PRE_TOPC: 13;

        consider Q2 be Subset of GX such that

         A32: Q2 is closed and

         A33: (Q2 /\ ( [#] X9)) = Q1 by A30, PRE_TOPC: 13;

        (Q2 /\ ( [#] (GX | A))) = (Q2 /\ (( [#] X9) /\ B)) by A1, A2, XBOOLE_1: 28

        .= QQ by A3, A31, A33, XBOOLE_1: 16;

        then

         A34: QQ is closed by A32, PRE_TOPC: 13;

        consider P2 be Subset of GX such that

         A35: P2 is closed and

         A36: (P2 /\ ( [#] X9)) = P1 by A28, PRE_TOPC: 13;

        (P2 /\ ( [#] (GX | A))) = (P2 /\ (( [#] X9) /\ B)) by A1, A2, XBOOLE_1: 28

        .= PP by A3, A29, A36, XBOOLE_1: 16;

        then PP is closed by A35, PRE_TOPC: 13;

        then not (GX9 | A9) is connected by A1, A2, A3, A22, A23, A24, A27, A34, Th10;

        hence not A is connected;

      end;

      hence thesis by A4;

    end;

    theorem :: CONNSP_1:24

    A is closed & B is closed & (A \/ B) is connected & (A /\ B) is connected implies A is connected & B is connected

    proof

      assume that

       A1: A is closed and

       A2: B is closed;

      set AB = (A \/ B);

      

       A3: (A \/ B) = ( [#] (GX | (A \/ B))) by PRE_TOPC:def 5;

      then

      reconsider B1 = B as Subset of (GX | AB) by XBOOLE_1: 7;

      reconsider A1 = A as Subset of (GX | AB) by A3, XBOOLE_1: 7;

      

       A4: (( [#] (GX | (A \/ B))) \ (A1 /\ B1)) = ((A1 \ B1) \/ (B1 \ A1)) by A3, XBOOLE_1: 55;

      (B /\ ( [#] (GX | (A \/ B)))) = B by A3, XBOOLE_1: 7, XBOOLE_1: 28;

      then

       A5: B1 is closed by A2, PRE_TOPC: 13;

      (A /\ ( [#] (GX | (A \/ B)))) = A by A3, XBOOLE_1: 7, XBOOLE_1: 28;

      then A1 is closed by A1, PRE_TOPC: 13;

      then

       A6: ((A1 \ B1),(B1 \ A1)) are_separated by A5, Th9;

      assume that

       A7: (A \/ B) is connected and

       A8: (A /\ B) is connected;

      

       A9: (GX | (A \/ B)) is connected by A7;

      

       A10: (A1 /\ B1) is connected by A8, Th23;

      ((A1 /\ B1) \/ (B1 \ A1)) = B1 by XBOOLE_1: 51;

      then

       A11: B1 is connected by A9, A4, A6, A10, Th20;

      ((A1 /\ B1) \/ (A1 \ B1)) = A1 by XBOOLE_1: 51;

      then A1 is connected by A9, A4, A6, A10, Th20;

      hence thesis by A11, Th23;

    end;

    theorem :: CONNSP_1:25

    

     Th25: for F be Subset-Family of GX st (for A be Subset of GX st A in F holds A is connected) & (ex A be Subset of GX st A <> ( {} GX) & A in F & (for B be Subset of GX st B in F & B <> A holds not (A,B) are_separated )) holds ( union F) is connected

    proof

      let F be Subset-Family of GX;

      assume that

       A1: for A be Subset of GX st A in F holds A is connected and

       A2: ex A be Subset of GX st A <> ( {} GX) & A in F & for B be Subset of GX st B in F & B <> A holds not (A,B) are_separated ;

      consider A1 be Subset of GX such that A1 <> ( {} GX) and

       A3: A1 in F and

       A4: for B be Subset of GX st B in F & B <> A1 holds not (A1,B) are_separated by A2;

      reconsider A1 as Subset of GX;

      now

        let P,Q be Subset of GX;

        assume that

         A5: ( union F) = (P \/ Q) and

         A6: (P,Q) are_separated ;

        P misses Q by A6, Th1;

        then

         A7: (P /\ Q) = {} ;

         A8:

        now

          assume

           A9: A1 c= Q;

          now

            let B be Subset of GX;

            assume that

             A10: B in F and B <> A1 and

             A11: not B c= Q;

            B is connected by A1, A10;

            then B c= P or B c= Q by A5, A6, A10, Th16, ZFMISC_1: 74;

            hence contradiction by A4, A6, A9, A10, A11, Th7;

          end;

          then for A be set st A in F holds A c= Q by A9;

          then

           A12: ( union F) c= Q by ZFMISC_1: 76;

          Q c= (P \/ Q) by XBOOLE_1: 7;

          then Q = (P \/ Q) by A5, A12;

          hence P = ( {} GX) by A7, XBOOLE_1: 7, XBOOLE_1: 28;

        end;

         A13:

        now

          assume

           A14: A1 c= P;

          now

            let B be Subset of GX;

            assume that

             A15: B in F and B <> A1;

            B is connected by A1, A15;

            then

             A16: B c= P or B c= Q by A5, A6, A15, Th16, ZFMISC_1: 74;

            assume not B c= P;

            hence contradiction by A4, A6, A14, A15, A16, Th7;

          end;

          then for A be set st A in F holds A c= P by A14;

          then

           A17: ( union F) c= P by ZFMISC_1: 76;

          P c= (P \/ Q) by XBOOLE_1: 7;

          then P = (P \/ Q) by A5, A17;

          hence Q = ( {} GX) by A7, XBOOLE_1: 7, XBOOLE_1: 28;

        end;

        A1 c= (P \/ Q) by A3, A5, ZFMISC_1: 74;

        hence P = ( {} GX) or Q = ( {} GX) by A1, A3, A6, A13, A8, Th16;

      end;

      hence thesis by Th15;

    end;

    theorem :: CONNSP_1:26

    

     Th26: for F be Subset-Family of GX st (for A be Subset of GX st A in F holds A is connected) & ( meet F) <> ( {} GX) holds ( union F) is connected

    proof

      let F be Subset-Family of GX;

      assume that

       A1: for A be Subset of GX st A in F holds A is connected and

       A2: ( meet F) <> ( {} GX);

      consider x be Point of GX such that

       A3: x in ( meet F) by A2, PRE_TOPC: 12;

      ( meet F) c= ( union F) by SETFAM_1: 2;

      then

      consider A2 be set such that

       A4: x in A2 and

       A5: A2 in F by A3, TARSKI:def 4;

      reconsider A2 as Subset of GX by A5;

       A6:

      now

        let B be Subset of GX such that

         A7: B in F and B <> A2;

        A2 c= ( Cl A2) by PRE_TOPC: 18;

        then x in ( Cl A2) & x in B or x in A2 & x in ( Cl B) by A3, A4, A7, SETFAM_1:def 1;

        then (( Cl A2) /\ B) <> {} or (A2 /\ ( Cl B)) <> {} by XBOOLE_0:def 4;

        then ( Cl A2) meets B or A2 meets ( Cl B);

        hence not (A2,B) are_separated ;

      end;

      A2 <> ( {} GX) by A4;

      hence thesis by A1, A5, A6, Th25;

    end;

    theorem :: CONNSP_1:27

    

     Th27: ( [#] GX) is connected iff GX is connected

    proof

      

       A1: ( [#] GX) = ( [#] (GX | ( [#] GX))) by PRE_TOPC:def 5;

       A2:

      now

        assume

         A3: GX is connected;

        now

          let P1,Q1 be Subset of (GX | ( [#] GX)) such that

           A4: ( [#] (GX | ( [#] GX))) = (P1 \/ Q1) and

           A5: (P1,Q1) are_separated ;

          reconsider Q = Q1 as Subset of GX by PRE_TOPC: 11;

          reconsider P = P1 as Subset of GX by PRE_TOPC: 11;

          (P,Q) are_separated by A5, Th5;

          hence P1 = ( {} (GX | ( [#] GX))) or Q1 = ( {} (GX | ( [#] GX))) by A1, A3, A4;

        end;

        then (GX | ( [#] GX)) is connected;

        hence ( [#] GX) is connected;

      end;

      now

        assume ( [#] GX) is connected;

        then

         A6: (GX | ( [#] GX)) is connected;

        now

          let P1,Q1 be Subset of GX such that

           A7: ( [#] GX) = (P1 \/ Q1) and

           A8: (P1,Q1) are_separated ;

          reconsider Q = Q1 as Subset of (GX | ( [#] GX)) by A1;

          reconsider P = P1 as Subset of (GX | ( [#] GX)) by A1;

          (P,Q) are_separated by A1, A7, A8, Th6;

          hence P1 = ( {} GX) or Q1 = ( {} GX) by A1, A6, A7;

        end;

        hence GX is connected;

      end;

      hence thesis by A2;

    end;

    registration

      let GX be non empty TopSpace, x be Point of GX;

      cluster {x} -> connected;

      coherence

      proof

        now

          assume not {x} is connected;

          then

          consider P,Q be Subset of GX such that

           A1: {x} = (P \/ Q) and

           A2: (P,Q) are_separated and

           A3: P <> ( {} GX) and

           A4: Q <> ( {} GX) by Th15;

          P <> Q

          proof

            assume not thesis;

            then

             A5: (P /\ Q) = P;

            P misses Q by A2, Th1;

            hence contradiction by A3, A5;

          end;

          hence contradiction by A1, A3, A4, ZFMISC_1: 38;

        end;

        hence thesis;

      end;

    end

    definition

      let GX be TopStruct, x,y be Point of GX;

      :: CONNSP_1:def4

      pred x,y are_joined means

      : Def4: ex C be Subset of GX st C is connected & x in C & y in C;

    end

    theorem :: CONNSP_1:28

    

     Th28: for GX be non empty TopSpace st ex x be Point of GX st for y be Point of GX holds (x,y) are_joined holds GX is connected

    proof

      let GX be non empty TopSpace;

      given a be Point of GX such that

       A1: for x be Point of GX holds (a,x) are_joined ;

      now

        let x be Point of GX;

        defpred P[ set] means ex C1 be Subset of GX st C1 = $1 & C1 is connected & x in $1;

        consider F be Subset-Family of GX such that

         A2: for C be Subset of GX holds C in F iff P[C] from SUBSET_1:sch 3;

        take F;

        let C be Subset of GX;

        thus C in F implies C is connected & x in C

        proof

          assume C in F;

          then ex C1 be Subset of GX st C1 = C & C1 is connected & x in C by A2;

          hence thesis;

        end;

        thus C is connected & x in C implies C in F by A2;

      end;

      then

      consider F be Subset-Family of GX such that

       A3: for C be Subset of GX holds C in F iff C is connected & a in C;

      

       A4: for x be Point of GX holds ex C be Subset of GX st C is connected & a in C & x in C by A1, Def4;

      now

        let x be object;

        assume x in ( [#] GX);

        then

        consider C be Subset of GX such that

         A5: C is connected and

         A6: a in C and

         A7: x in C by A4;

        C in F by A3, A5, A6;

        hence x in ( union F) by A7, TARSKI:def 4;

      end;

      then ( [#] GX) c= ( union F) by TARSKI:def 3;

      then

       A8: ( union F) = ( [#] GX);

      

       A9: for A be set st A in F holds a in A by A3;

      a in {a} by TARSKI:def 1;

      then F <> {} by A3;

      then

       A10: ( meet F) <> ( {} GX) by A9, SETFAM_1:def 1;

      for A be Subset of GX st A in F holds A is connected by A3;

      then ( [#] GX) is connected by A8, A10, Th26;

      hence thesis by Th27;

    end;

    theorem :: CONNSP_1:29

    

     Th29: (ex x be Point of GX st for y be Point of GX holds (x,y) are_joined ) iff for x,y be Point of GX holds (x,y) are_joined

    proof

       A1:

      now

        given a be Point of GX such that

         A2: for x be Point of GX holds (a,x) are_joined ;

        let x,y be Point of GX;

        (a,x) are_joined by A2;

        then

        consider C1 be Subset of GX such that

         A3: C1 is connected and

         A4: a in C1 and

         A5: x in C1;

        (a,y) are_joined by A2;

        then

        consider C2 be Subset of GX such that

         A6: C2 is connected and

         A7: a in C2 and

         A8: y in C2;

        (C1 /\ C2) <> ( {} GX) by A4, A7, XBOOLE_0:def 4;

        then C1 meets C2;

        then

         A9: (C1 \/ C2) is connected by A3, A6, Th1, Th17;

        

         A10: y in (C1 \/ C2) by A8, XBOOLE_0:def 3;

        x in (C1 \/ C2) by A5, XBOOLE_0:def 3;

        hence (x,y) are_joined by A9, A10;

      end;

      now

        set a = the Point of GX;

        assume for x,y be Point of GX holds (x,y) are_joined ;

        then for y be Point of GX holds (a,y) are_joined ;

        hence ex x be Point of GX st for y be Point of GX holds (x,y) are_joined ;

      end;

      hence thesis by A1;

    end;

    theorem :: CONNSP_1:30

    for GX be non empty TopSpace st for x,y be Point of GX holds (x,y) are_joined holds GX is connected

    proof

      let GX be non empty TopSpace;

      assume for x,y be Point of GX holds (x,y) are_joined ;

      then ex x be Point of GX st for y be Point of GX holds (x,y) are_joined by Th29;

      hence thesis by Th28;

    end;

    theorem :: CONNSP_1:31

    

     Th31: for GX be non empty TopSpace holds for x be Point of GX, F be Subset-Family of GX st for A be Subset of GX holds A in F iff A is connected & x in A holds F <> {}

    proof

      let GX be non empty TopSpace;

      let x be Point of GX, F be Subset-Family of GX such that

       A1: for A be Subset of GX holds A in F iff A is connected & x in A;

      x in {x} by TARSKI:def 1;

      hence thesis by A1;

    end;

    definition

      let GX be TopStruct, A be Subset of GX;

      :: CONNSP_1:def5

      attr A is a_component means A is connected & for B be Subset of GX st B is connected holds A c= B implies A = B;

    end

    registration

      let GX be TopStruct;

      cluster a_component -> connected for Subset of GX;

      coherence ;

    end

    registration

      let GX be non empty TopSpace;

      cluster a_component -> non empty for Subset of GX;

      coherence

      proof

         {} c= { the Point of GX} by XBOOLE_1: 2;

        hence thesis;

      end;

    end

    theorem :: CONNSP_1:32

    for GX be non empty TopSpace, A be Subset of GX st A is a_component holds A <> ( {} GX);

    registration

      let GX;

      cluster a_component -> closed for Subset of GX;

      coherence

      proof

        let A;

        

         A1: A c= ( Cl A) by PRE_TOPC: 18;

        assume

         A2: A is a_component;

        then ( Cl A) is connected by Th19;

        then A = ( Cl A) by A2, A1;

        hence thesis by PRE_TOPC: 22;

      end;

    end

    theorem :: CONNSP_1:33

    A is a_component implies A is closed;

    theorem :: CONNSP_1:34

    

     Th34: A is a_component & B is a_component implies A = B or (A,B) are_separated

    proof

      assume that

       A1: A is a_component and

       A2: B is a_component;

      A <> B implies (A,B) are_separated

      proof

        

         A3: B c= (A \/ B) by XBOOLE_1: 7;

        

         A4: A c= (A \/ B) by XBOOLE_1: 7;

        assume

         A5: A <> B;

        assume not (A,B) are_separated ;

        then (A \/ B) is connected by A1, A2, Th17;

        then A = (A \/ B) by A1, A4;

        hence contradiction by A1, A2, A5, A3;

      end;

      hence thesis;

    end;

    theorem :: CONNSP_1:35

    A is a_component & B is a_component implies A = B or A misses B by Th1, Th34;

    theorem :: CONNSP_1:36

    C is connected implies for S be Subset of GX st S is a_component holds C misses S or C c= S

    proof

      assume

       A1: C is connected;

      let S be Subset of GX;

      assume

       A2: S is a_component;

      

       A3: S c= (C \/ S) by XBOOLE_1: 7;

      assume C meets S;

      then (C \/ S) is connected by A1, A2, Th1, Th17;

      then S = (C \/ S) by A2, A3;

      hence thesis by XBOOLE_1: 7;

    end;

    definition

      let GX be TopStruct, A,B be Subset of GX;

      :: CONNSP_1:def6

      pred B is_a_component_of A means ex B1 be Subset of (GX | A) st B1 = B & B1 is a_component;

    end

    theorem :: CONNSP_1:37

    GX is connected & A is connected & C is_a_component_of (( [#] GX) \ A) implies (( [#] GX) \ C) is connected

    proof

      assume that

       A1: GX is connected and

       A2: A is connected and

       A3: C is_a_component_of (( [#] GX) \ A);

      consider C1 be Subset of (GX | (( [#] GX) \ A)) such that

       A4: C1 = C and

       A5: C1 is a_component by A3;

      reconsider C2 = C1 as Subset of GX by A4;

      C1 c= ( [#] (GX | (( [#] GX) \ A)));

      then C1 c= (( [#] GX) \ A) by PRE_TOPC:def 5;

      then ((( [#] GX) \ A) ` ) c= (C2 ` ) by SUBSET_1: 12;

      then

       A6: A c= (C2 ` ) by PRE_TOPC: 3;

      now

        A misses C1 by A6, SUBSET_1: 23;

        then

         A7: (A /\ C1) = {} ;

        

         A8: C is connected by A4, A5, Th23;

        let P,Q be Subset of GX such that

         A9: (( [#] GX) \ C) = (P \/ Q) and

         A10: (P,Q) are_separated ;

        

         A11: P misses (P ` ) by XBOOLE_1: 79;

        

         A12: P misses Q by A10, Th1;

         A13:

        now

          

           A14: Q misses (Q ` ) by XBOOLE_1: 79;

          assume

           A15: A c= Q;

          P c= (Q ` ) by A12, SUBSET_1: 23;

          then (A /\ P) c= (Q /\ (Q ` )) by A15, XBOOLE_1: 27;

          then

           A16: (A /\ P) c= {} by A14;

          ((C \/ P) /\ A) = ((A /\ C) \/ (A /\ P)) by XBOOLE_1: 23

          .= {} by A4, A7, A16;

          then (C \/ P) misses A;

          then (C \/ P) c= (A ` ) by SUBSET_1: 23;

          then (C \/ P) c= ( [#] (GX | (( [#] GX) \ A))) by PRE_TOPC:def 5;

          then

          reconsider C1P1 = (C \/ P) as Subset of (GX | (( [#] GX) \ A));

          

           A17: C misses (C ` ) by XBOOLE_1: 79;

          (C \/ P) is connected by A1, A9, A10, A8, Th20;

          then

           A18: C1P1 is connected by Th23;

          C c= (C1 \/ P) by A4, XBOOLE_1: 7;

          then C1P1 = C1 by A4, A5, A18;

          then

           A19: P c= C by A4, XBOOLE_1: 7;

          P c= (( [#] GX) \ C) by A9, XBOOLE_1: 7;

          then P c= (C /\ (( [#] GX) \ C)) by A19, XBOOLE_1: 19;

          then P c= {} by A17;

          hence P = ( {} GX);

        end;

        

         A20: Q c= (( [#] GX) \ C) by A9, XBOOLE_1: 7;

        now

          assume

           A21: A c= P;

          Q c= (P ` ) by A12, SUBSET_1: 23;

          then (A /\ Q) c= (P /\ (P ` )) by A21, XBOOLE_1: 27;

          then

           A22: (A /\ Q) c= {} by A11;

          ((C \/ Q) /\ A) = ((A /\ C) \/ (A /\ Q)) by XBOOLE_1: 23

          .= {} by A4, A7, A22;

          then (C \/ Q) misses A;

          then (C \/ Q) c= (A ` ) by SUBSET_1: 23;

          then (C \/ Q) c= ( [#] (GX | (( [#] GX) \ A))) by PRE_TOPC:def 5;

          then

          reconsider C1Q1 = (C \/ Q) as Subset of (GX | (( [#] GX) \ A));

          (C \/ Q) is connected by A1, A9, A10, A8, Th20;

          then

           A23: C1Q1 is connected by Th23;

          C1 c= (C1 \/ Q) by XBOOLE_1: 7;

          then C1Q1 = C1 by A4, A5, A23;

          then Q c= C by A4, XBOOLE_1: 7;

          then

           A24: Q c= (C /\ (( [#] GX) \ C)) by A20, XBOOLE_1: 19;

          C misses (C ` ) by XBOOLE_1: 79;

          then Q c= {} by A24;

          hence Q = ( {} GX);

        end;

        hence P = ( {} GX) or Q = ( {} GX) by A2, A4, A6, A9, A10, A13, Th16;

      end;

      hence thesis by Th15;

    end;

    definition

      let GX be TopStruct, x be Point of GX;

      :: CONNSP_1:def7

      func Component_of x -> Subset of GX means

      : Def7: ex F be Subset-Family of GX st (for A be Subset of GX holds A in F iff A is connected & x in A) & ( union F) = it ;

      existence

      proof

        defpred P[ set] means ex A1 be Subset of GX st A1 = $1 & A1 is connected & x in $1;

        consider F be Subset-Family of GX such that

         A1: for A be Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3;

        take ( union F), F;

        thus for A be Subset of GX holds A in F iff A is connected & x in A

        proof

          let A be Subset of GX;

          thus A in F implies A is connected & x in A

          proof

            assume A in F;

            then ex A1 be Subset of GX st A1 = A & A1 is connected & x in A by A1;

            hence thesis;

          end;

          thus thesis by A1;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let S,S9 be Subset of GX;

        assume that

         A2: ex F be Subset-Family of GX st (for A be Subset of GX holds A in F iff A is connected & x in A) & ( union F) = S and

         A3: ex F9 be Subset-Family of GX st (for A be Subset of GX holds A in F9 iff A is connected & x in A) & ( union F9) = S9;

        consider F be Subset-Family of GX such that

         A4: for A be Subset of GX holds A in F iff A is connected & x in A and

         A5: ( union F) = S by A2;

        consider F9 be Subset-Family of GX such that

         A6: for A be Subset of GX holds A in F9 iff A is connected & x in A and

         A7: ( union F9) = S9 by A3;

        now

          let y be object;

           A8:

          now

            assume y in S9;

            then

            consider B be set such that

             A9: y in B and

             A10: B in F9 by A7, TARSKI:def 4;

            reconsider B as Subset of GX by A10;

            

             A11: x in B by A6, A10;

            B is connected by A6, A10;

            then B in F by A4, A11;

            hence y in S by A5, A9, TARSKI:def 4;

          end;

          now

            assume y in S;

            then

            consider B be set such that

             A12: y in B and

             A13: B in F by A5, TARSKI:def 4;

            reconsider B as Subset of GX by A13;

            

             A14: x in B by A4, A13;

            B is connected by A4, A13;

            then B in F9 by A6, A14;

            hence y in S9 by A7, A12, TARSKI:def 4;

          end;

          hence y in S iff y in S9 by A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    reserve GX for non empty TopSpace;

    reserve A,C for Subset of GX;

    reserve x for Point of GX;

    theorem :: CONNSP_1:38

    

     Th38: x in ( Component_of x)

    proof

      consider F be Subset-Family of GX such that

       A1: for A be Subset of GX holds A in F iff A is connected & x in A and

       A2: ( Component_of x) = ( union F) by Def7;

      

       A3: for A be set holds A in F implies x in A by A1;

      F <> {} by A1, Th31;

      then

       A4: x in ( meet F) by A3, SETFAM_1:def 1;

      ( meet F) c= ( union F) by SETFAM_1: 2;

      hence thesis by A2, A4;

    end;

    registration

      let GX, x;

      cluster ( Component_of x) -> non empty connected;

      coherence

      proof

        consider F be Subset-Family of GX such that

         A1: for A be Subset of GX holds A in F iff A is connected & x in A and

         A2: ( Component_of x) = ( union F) by Def7;

        

         A3: for A be set holds A in F implies x in A by A1;

        F <> {} by A1, Th31;

        then

         A4: ( meet F) <> ( {} GX) by A3, SETFAM_1:def 1;

        for A be Subset of GX st A in F holds A is connected by A1;

        hence thesis by A2, A4, Th26, Th38;

      end;

    end

    theorem :: CONNSP_1:39

    

     Th39: C is connected & ( Component_of x) c= C implies C = ( Component_of x)

    proof

      assume

       A1: C is connected;

      consider F be Subset-Family of GX such that

       A2: for A be Subset of GX holds (A in F iff A is connected & x in A) and

       A3: ( Component_of x) = ( union F) by Def7;

      assume

       A4: ( Component_of x) c= C;

      x in ( Component_of x) by Th38;

      then C in F by A1, A4, A2;

      then C c= ( Component_of x) by A3, ZFMISC_1: 74;

      hence thesis by A4;

    end;

    theorem :: CONNSP_1:40

    

     Th40: A is a_component iff ex x be Point of GX st A = ( Component_of x)

    proof

      hereby

        assume

         A1: A is a_component;

        then A <> ( {} GX);

        then

        consider y be Point of GX such that

         A2: y in A by PRE_TOPC: 12;

        take x = y;

        consider F be Subset-Family of GX such that

         A3: for B be Subset of GX holds B in F iff B is connected & x in B and

         A4: ( union F) = ( Component_of x) by Def7;

        A in F by A1, A2, A3;

        then A c= ( union F) by ZFMISC_1: 74;

        hence A = ( Component_of x) by A1, A4;

      end;

      given x be Point of GX such that

       A5: A = ( Component_of x);

      for B be Subset of GX st B is connected holds A c= B implies A = B by A5, Th39;

      hence A is a_component by A5;

    end;

    theorem :: CONNSP_1:41

    A is a_component & x in A implies A = ( Component_of x)

    proof

      assume that

       A1: A is a_component and

       A2: x in A;

      x in ( Component_of x) by Th38;

      then (A /\ ( Component_of x)) <> {} by A2, XBOOLE_0:def 4;

      then

       A3: A meets ( Component_of x);

      

       A4: ( Component_of x) is a_component by Th40;

      assume A <> ( Component_of x);

      hence contradiction by A1, A3, A4, Th1, Th34;

    end;

    theorem :: CONNSP_1:42

    for p be Point of GX st p in ( Component_of x) holds ( Component_of p) = ( Component_of x)

    proof

      set A = ( Component_of x);

      

       A1: A is a_component by Th40;

      given p be Point of GX such that

       A2: p in A and

       A3: ( Component_of p) <> A;

      ( Component_of p) is a_component by Th40;

      then ( Component_of p) misses A by A3, A1, Th1, Th34;

      then

       A4: (( Component_of p) /\ A) = ( {} GX);

      p in ( Component_of p) by Th38;

      hence contradiction by A2, A4, XBOOLE_0:def 4;

    end;

    theorem :: CONNSP_1:43

    for F be Subset-Family of GX st for A be Subset of GX holds A in F iff A is a_component holds F is Cover of GX

    proof

      let F be Subset-Family of GX such that

       A1: for A be Subset of GX holds A in F iff A is a_component;

      now

        let x be object;

        assume x in ( [#] GX);

        then

        reconsider y = x as Point of GX;

        ( Component_of y) is a_component by Th40;

        then ( Component_of y) in F by A1;

        then

         A2: ( Component_of y) c= ( union F) by ZFMISC_1: 74;

        y in ( Component_of y) by Th38;

        hence x in ( union F) by A2;

      end;

      then ( [#] GX) c= ( union F) by TARSKI:def 3;

      hence thesis by SETFAM_1:def 11;

    end;

    begin

    registration

      let T be TopStruct;

      cluster empty for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    registration

      let T be TopStruct;

      cluster empty -> connected for Subset of T;

      coherence

      proof

        let C be Subset of T;

        assume C is empty;

        then

        reconsider D = C as empty Subset of T;

        let A,B be Subset of (T | C) such that ( [#] (T | C)) = (A \/ B) and (A,B) are_separated ;

        ( [#] (T | D)) = {} ;

        hence thesis;

      end;

    end

    theorem :: CONNSP_1:44

    

     Th44: for T be TopSpace, X be set holds X is connected Subset of T iff X is connected Subset of the TopStruct of T

    proof

      let T be TopSpace, X be set;

      thus X is connected Subset of T implies X is connected Subset of the TopStruct of T

      proof

        assume

         A1: X is connected Subset of T;

        then

        reconsider X as Subset of T;

        reconsider Y = X as Subset of the TopStruct of T;

         the TopStruct of (T | X) = ( the TopStruct of T | Y) by PRE_TOPC: 36;

        then ( the TopStruct of T | Y) is connected by A1, Def3;

        hence thesis by Def3;

      end;

      assume

       A2: X is connected Subset of the TopStruct of T;

      then

      reconsider X as Subset of the TopStruct of T;

      reconsider Y = X as Subset of T;

       the TopStruct of (T | Y) = ( the TopStruct of T | X) by PRE_TOPC: 36;

      then (T | Y) is connected by A2, Def3;

      hence thesis by Def3;

    end;

    theorem :: CONNSP_1:45

    for T be TopSpace, X be Subset of T, Y be Subset of the TopStruct of T st X = Y holds X is a_component iff Y is a_component by Th44;

    theorem :: CONNSP_1:46

    for G be non empty TopSpace, P be Subset of G, A be Subset of G, Q be Subset of (G | A) st P = Q & P is connected holds Q is connected

    proof

      let G be non empty TopSpace, P be Subset of G, A be Subset of G, Q be Subset of (G | A);

      assume that

       A1: P = Q and

       A2: P is connected;

      

       A3: (G | P) is connected by A2;

      Q c= the carrier of (G | A);

      then Q c= A by PRE_TOPC: 8;

      then (G | P) = ((G | A) | Q) by A1, PRE_TOPC: 7;

      hence thesis by A3;

    end;