tsep_2.miz



    begin

    reserve X for non empty 1-sorted;

    theorem :: TSEP_2:1

    

     Th1: for A,B be Subset of X holds ((A ` ) \ (B ` )) = (B \ A)

    proof

      let A,B be Subset of X;

      ((A ` ) \ (B ` )) = (( [#] X) \ (A \/ (B ` ))) by XBOOLE_1: 41;

      then ((A ` ) \ (B ` )) = ((A ` ) /\ ((B ` ) ` )) by XBOOLE_1: 53;

      hence thesis by SUBSET_1: 13;

    end;

    definition

      let X be 1-sorted, A1,A2 be Subset of X;

      :: TSEP_2:def1

      pred A1,A2 constitute_a_decomposition means A1 misses A2 & (A1 \/ A2) = the carrier of X;

      symmetry ;

    end

    notation

      let X be 1-sorted, A1,A2 be Subset of X;

      antonym A1,A2 do_not_constitute_a_decomposition for A1,A2 constitute_a_decomposition ;

    end

    reserve A,A1,A2,B1,B2 for Subset of X;

    theorem :: TSEP_2:2

    (A1,A2) constitute_a_decomposition iff A1 misses A2 & (A1 \/ A2) = ( [#] X);

    theorem :: TSEP_2:3

    

     Th3: (A1,A2) constitute_a_decomposition implies A1 = (A2 ` ) & A2 = (A1 ` )

    proof

      assume

       A1: (A1,A2) constitute_a_decomposition ;

      then

       A2: A1 misses A2;

      then

       A3: A1 c= (A2 ` ) by SUBSET_1: 23;

      

       A4: A2 c= (A1 ` ) by A2, SUBSET_1: 23;

      

       A5: (A1 \/ A2) = ( [#] X) by A1;

      then (A2 ` ) c= A1 by TDLAT_1: 1;

      hence A1 = (A2 ` ) by A3;

      (A1 ` ) c= A2 by A5, TDLAT_1: 1;

      hence thesis by A4;

    end;

    theorem :: TSEP_2:4

    

     Th4: A1 = (A2 ` ) or A2 = (A1 ` ) implies (A1,A2) constitute_a_decomposition

    proof

      assume A1 = (A2 ` ) or A2 = (A1 ` );

      then A1 misses A2 & (A1 \/ A2) = ( [#] X) by SUBSET_1: 23, TDLAT_1: 1;

      hence thesis;

    end;

    theorem :: TSEP_2:5

    

     Th5: (A,(A ` )) constitute_a_decomposition

    proof

      A misses (A ` ) & (A \/ (A ` )) = ( [#] X) by PRE_TOPC: 2, XBOOLE_1: 79;

      hence (A,(A ` )) constitute_a_decomposition ;

    end;

    theorem :: TSEP_2:6

    (( {} X),( [#] X)) constitute_a_decomposition

    proof

      ( [#] X) = (( {} X) ` );

      hence (( {} X),( [#] X)) constitute_a_decomposition by Th5;

    end;

    theorem :: TSEP_2:7

    

     Th7: (A,A) do_not_constitute_a_decomposition

    proof

      assume

       A1: (A,A) constitute_a_decomposition ;

      per cases ;

        suppose

         A2: A is non empty;

        A = (A ` ) by A1, Th3;

        then A misses A by SUBSET_1: 23;

        then (A /\ A) = {} ;

        hence contradiction by A2;

      end;

        suppose A is empty;

        

        then {} = (A \/ A)

        .= the carrier of X by A1;

        hence contradiction;

      end;

    end;

    definition

      let X be non empty 1-sorted, A1,A2 be Subset of X;

      :: original: constitute_a_decomposition

      redefine

      pred A1,A2 constitute_a_decomposition ;

      irreflexivity by Th7;

    end

    theorem :: TSEP_2:8

    

     Th8: (A1,A) constitute_a_decomposition & (A,A2) constitute_a_decomposition implies A1 = A2

    proof

      assume (A1,A) constitute_a_decomposition ;

      then

       A1: A1 = (A ` ) by Th3;

      assume (A,A2) constitute_a_decomposition ;

      hence thesis by A1, Th3;

    end;

    reserve X for non empty TopSpace;

    reserve A,A1,A2,B1,B2 for Subset of X;

    theorem :: TSEP_2:9

    

     Th9: (A1,A2) constitute_a_decomposition implies (( Cl A1),( Int A2)) constitute_a_decomposition & (( Int A1),( Cl A2)) constitute_a_decomposition

    proof

      assume

       A1: (A1,A2) constitute_a_decomposition ;

      ( Cl A1) = (( Int (A1 ` )) ` ) by TDLAT_3: 1;

      then ( Cl A1) = (( Int A2) ` ) by A1, Th3;

      hence (( Cl A1),( Int A2)) constitute_a_decomposition by Th4;

      ( Int A1) = (( Cl (A1 ` )) ` ) by TOPS_1:def 1;

      then ( Int A1) = (( Cl A2) ` ) by A1, Th3;

      hence (( Int A1),( Cl A2)) constitute_a_decomposition by Th4;

    end;

    theorem :: TSEP_2:10

    (( Cl A),( Int (A ` ))) constitute_a_decomposition & (( Cl (A ` )),( Int A)) constitute_a_decomposition & (( Int A),( Cl (A ` ))) constitute_a_decomposition & (( Int (A ` )),( Cl A)) constitute_a_decomposition

    proof

      

       A1: (A,(A ` )) constitute_a_decomposition by Th5;

      hence (( Cl A),( Int (A ` ))) constitute_a_decomposition by Th9;

      

       A2: ((A ` ),A) constitute_a_decomposition by Th5;

      hence (( Cl (A ` )),( Int A)) constitute_a_decomposition by Th9;

      thus (( Int A),( Cl (A ` ))) constitute_a_decomposition by A2, Th9;

      thus thesis by A1, Th9;

    end;

    theorem :: TSEP_2:11

    

     Th11: for A1,A2 be Subset of X st (A1,A2) constitute_a_decomposition holds (A1 is open iff A2 is closed)

    proof

      let A1,A2 be Subset of X;

      assume

       A1: (A1,A2) constitute_a_decomposition ;

      then A2 = (A1 ` ) by Th3;

      hence A1 is open implies A2 is closed by TOPS_1: 4;

      assume

       A2: A2 is closed;

      A1 = (A2 ` ) by A1, Th3;

      hence thesis by A2, TOPS_1: 3;

    end;

    theorem :: TSEP_2:12

    for A1,A2 be Subset of X st (A1,A2) constitute_a_decomposition holds (A1 is closed iff A2 is open) by Th11;

    reserve X for non empty 1-sorted;

    reserve A,A1,A2,B1,B2 for Subset of X;

    theorem :: TSEP_2:13

    

     Th13: (A1,A2) constitute_a_decomposition & (B1,B2) constitute_a_decomposition implies ((A1 /\ B1),(A2 \/ B2)) constitute_a_decomposition

    proof

      assume

       A1: (A1,A2) constitute_a_decomposition ;

      then A1 misses A2;

      then

       A2: (A1 /\ A2) = {} ;

      assume

       A3: (B1,B2) constitute_a_decomposition ;

      then

       A4: (B1 \/ B2) = ( [#] X);

      B1 misses B2 by A3;

      then

       A5: (B1 /\ B2) = ( {} X);

      ((A1 /\ B1) /\ (A2 \/ B2)) = (((B1 /\ A1) /\ A2) \/ ((A1 /\ B1) /\ B2)) by XBOOLE_1: 23

      .= ((B1 /\ (A1 /\ A2)) \/ ((A1 /\ B1) /\ B2)) by XBOOLE_1: 16

      .= ((B1 /\ (A1 /\ A2)) \/ (A1 /\ (B1 /\ B2))) by XBOOLE_1: 16

      .= ( {} X) by A5, A2;

      then

       A6: (A1 /\ B1) misses (A2 \/ B2);

      ((A1 /\ B1) \/ (A2 \/ B2)) = ((A1 \/ (A2 \/ B2)) /\ (B1 \/ (A2 \/ B2))) by XBOOLE_1: 24

      .= (((A1 \/ A2) \/ B2) /\ (B1 \/ (B2 \/ A2))) by XBOOLE_1: 4

      .= (((A1 \/ A2) \/ B2) /\ ((B1 \/ B2) \/ A2)) by XBOOLE_1: 4

      .= ((( [#] X) \/ B2) /\ (( [#] X) \/ A2)) by A1, A4

      .= ((( [#] X) \/ B2) /\ ( [#] X)) by XBOOLE_1: 12

      .= (( [#] X) /\ ( [#] X)) by XBOOLE_1: 12

      .= ( [#] X);

      hence thesis by A6;

    end;

    theorem :: TSEP_2:14

    (A1,A2) constitute_a_decomposition & (B1,B2) constitute_a_decomposition implies ((A1 \/ B1),(A2 /\ B2)) constitute_a_decomposition by Th13;

    begin

    reserve X for non empty TopSpace,

A1,A2 for Subset of X;

    theorem :: TSEP_2:15

    

     Th15: for A1,A2,C1,C2 be Subset of X st (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition holds (A1,A2) are_weakly_separated iff (C1,C2) are_weakly_separated

    proof

      let A1,A2,C1,C2 be Subset of X;

      assume (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition ;

      then

       A1: C1 = (A1 ` ) & C2 = (A2 ` ) by Th3;

      thus (A1,A2) are_weakly_separated implies (C1,C2) are_weakly_separated

      proof

        assume ((A1 \ A2),(A2 \ A1)) are_separated ;

        then ((C2 \ C1),((C2 ` ) \ (C1 ` ))) are_separated by A1, Th1;

        then ((C2 \ C1),(C1 \ C2)) are_separated by Th1;

        hence thesis;

      end;

      assume (C1,C2) are_weakly_separated ;

      then ((C1 \ C2),(C2 \ C1)) are_separated ;

      then (((C2 ` ) \ (C1 ` )),(C2 \ C1)) are_separated by Th1;

      then ((A2 \ A1),(A1 \ A2)) are_separated by A1, Th1;

      hence thesis;

    end;

    theorem :: TSEP_2:16

    (A1,A2) are_weakly_separated iff ((A1 ` ),(A2 ` )) are_weakly_separated

    proof

      (A1,(A1 ` )) constitute_a_decomposition & (A2,(A2 ` )) constitute_a_decomposition by Th5;

      hence thesis by Th15;

    end;

    theorem :: TSEP_2:17

    for A1,A2,C1,C2 be Subset of X st (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition holds (A1,A2) are_separated implies (C1,C2) are_weakly_separated

    proof

      let A1,A2,C1,C2 be Subset of X;

      assume

       A1: (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition ;

      assume (A1,A2) are_separated ;

      then (A1,A2) are_weakly_separated by TSEP_1: 46;

      hence thesis by A1, Th15;

    end;

    theorem :: TSEP_2:18

    

     Th18: for A1,A2,C1,C2 be Subset of X st (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition holds A1 misses A2 & (C1,C2) are_weakly_separated implies (A1,A2) are_separated

    proof

      let A1,A2,C1,C2 be Subset of X;

      assume

       A1: (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition ;

      assume

       A2: (A1 /\ A2) = {} ;

      assume (C1,C2) are_weakly_separated ;

      then

       A3: (A1,A2) are_weakly_separated by A1, Th15;

      A1 misses A2 by A2;

      hence thesis by A3, TSEP_1: 46;

    end;

    theorem :: TSEP_2:19

    for A1,A2,C1,C2 be Subset of X st (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition holds (C1 \/ C2) = the carrier of X & (C1,C2) are_weakly_separated implies (A1,A2) are_separated

    proof

      let A1,A2,C1,C2 be Subset of X;

      assume

       A1: (A1,C1) constitute_a_decomposition & (A2,C2) constitute_a_decomposition ;

      assume (C1 \/ C2) = the carrier of X;

      then

       A2: ((C1 \/ C2) ` ) = ( {} X) by XBOOLE_1: 37;

      A1 = (C1 ` ) & A2 = (C2 ` ) by A1, Th3;

      then (A1 /\ A2) = {} by A2, XBOOLE_1: 53;

      then

       A3: A1 misses A2;

      assume (C1,C2) are_weakly_separated ;

      hence thesis by A1, A3, Th18;

    end;

    theorem :: TSEP_2:20

    (A1,A2) constitute_a_decomposition implies ((A1,A2) are_weakly_separated iff (A1,A2) are_separated ) by TSEP_1: 46;

    theorem :: TSEP_2:21

    

     Th21: (A1,A2) are_weakly_separated iff (((A1 \/ A2) \ A1),((A1 \/ A2) \ A2)) are_separated

    proof

      

       A1: ((A1 \/ A2) \ A1) = (A2 \ A1) & ((A1 \/ A2) \ A2) = (A1 \ A2) by XBOOLE_1: 40;

      thus (A1,A2) are_weakly_separated implies (((A1 \/ A2) \ A1),((A1 \/ A2) \ A2)) are_separated by A1;

      assume (((A1 \/ A2) \ A1),((A1 \/ A2) \ A2)) are_separated ;

      hence thesis by A1;

    end;

    theorem :: TSEP_2:22

    

     Th22: for A1,A2,C1,C2 be Subset of X st C1 c= A1 & C2 c= A2 & (C1 \/ C2) = (A1 \/ A2) holds (C1,C2) are_weakly_separated implies (A1,A2) are_weakly_separated

    proof

      let A1,A2,C1,C2 be Subset of X;

      assume C1 c= A1 & C2 c= A2;

      then

       A1: ((A1 \/ A2) \ A1) c= ((A1 \/ A2) \ C1) & ((A1 \/ A2) \ A2) c= ((A1 \/ A2) \ C2) by XBOOLE_1: 34;

      assume

       A2: (C1 \/ C2) = (A1 \/ A2);

      assume (C1,C2) are_weakly_separated ;

      then (((A1 \/ A2) \ C1),((A1 \/ A2) \ C2)) are_separated by A2, Th21;

      then (((A1 \/ A2) \ A1),((A1 \/ A2) \ A2)) are_separated by A1, CONNSP_1: 7;

      hence thesis by Th21;

    end;

    theorem :: TSEP_2:23

    

     Th23: (A1,A2) are_weakly_separated iff ((A1 \ (A1 /\ A2)),(A2 \ (A1 /\ A2))) are_separated

    proof

      

       A1: (A2 \ (A1 /\ A2)) = (A2 \ A1) by XBOOLE_1: 47;

      

       A2: (A1 \ (A1 /\ A2)) = (A1 \ A2) by XBOOLE_1: 47;

      thus (A1,A2) are_weakly_separated implies ((A1 \ (A1 /\ A2)),(A2 \ (A1 /\ A2))) are_separated by A2, XBOOLE_1: 47;

      assume ((A1 \ (A1 /\ A2)),(A2 \ (A1 /\ A2))) are_separated ;

      hence thesis by A2, A1;

    end;

    theorem :: TSEP_2:24

    

     Th24: for A1,A2,C1,C2 be Subset of X st C1 c= A1 & C2 c= A2 & (C1 /\ C2) = (A1 /\ A2) holds (A1,A2) are_weakly_separated implies (C1,C2) are_weakly_separated

    proof

      let A1,A2,C1,C2 be Subset of X;

      assume C1 c= A1 & C2 c= A2;

      then

       A1: (C1 \ (C1 /\ C2)) c= (A1 \ (C1 /\ C2)) & (C2 \ (C1 /\ C2)) c= (A2 \ (C1 /\ C2)) by XBOOLE_1: 33;

      assume

       A2: (C1 /\ C2) = (A1 /\ A2);

      assume (A1,A2) are_weakly_separated ;

      then ((A1 \ (C1 /\ C2)),(A2 \ (C1 /\ C2))) are_separated by A2, Th23;

      then ((C1 \ (C1 /\ C2)),(C2 \ (C1 /\ C2))) are_separated by A1, CONNSP_1: 7;

      hence thesis by Th23;

    end;

    reserve X0 for non empty SubSpace of X,

B1,B2 for Subset of X0;

    theorem :: TSEP_2:25

    

     Th25: B1 = A1 & B2 = A2 implies ((A1,A2) are_separated iff (B1,B2) are_separated )

    proof

      assume that

       A1: B1 = A1 and

       A2: B2 = A2;

      

       A3: ( Cl B2) = (( Cl A2) /\ ( [#] X0)) by A2, PRE_TOPC: 17;

      

       A4: ( Cl B1) = (( Cl A1) /\ ( [#] X0)) by A1, PRE_TOPC: 17;

      thus (A1,A2) are_separated implies (B1,B2) are_separated

      proof

        assume

         A5: (A1,A2) are_separated ;

        then A1 misses ( Cl A2) by CONNSP_1:def 1;

        then (A1 /\ ( Cl A2)) = {} ;

        then (B1 /\ ( Cl B2)) = ( {} /\ ( [#] X0)) by A1, A3, XBOOLE_1: 16;

        then

         A6: B1 misses ( Cl B2);

        ( Cl A1) misses A2 by A5, CONNSP_1:def 1;

        then (( Cl A1) /\ A2) = {} ;

        then (( Cl B1) /\ B2) = ( {} /\ ( [#] X0)) by A2, A4, XBOOLE_1: 16;

        then ( Cl B1) misses B2;

        hence thesis by A6, CONNSP_1:def 1;

      end;

      thus (B1,B2) are_separated implies (A1,A2) are_separated

      proof

        assume

         A7: (B1,B2) are_separated ;

        then (( Cl A1) /\ ( [#] X0)) misses A2 by A2, A4, CONNSP_1:def 1;

        then ((( Cl A1) /\ ( [#] X0)) /\ A2) = {} ;

        then

         A8: ((( Cl A1) /\ A2) /\ ( [#] X0)) = {} by XBOOLE_1: 16;

        A1 misses (( Cl A2) /\ ( [#] X0)) by A1, A3, A7, CONNSP_1:def 1;

        then (A1 /\ (( Cl A2) /\ ( [#] X0))) = {} ;

        then

         A9: ((A1 /\ ( Cl A2)) /\ ( [#] X0)) = {} by XBOOLE_1: 16;

        (A1 /\ ( Cl A2)) c= A1 by XBOOLE_1: 17;

        then (A1 /\ ( Cl A2)) = {} by A1, A9, XBOOLE_1: 1, XBOOLE_1: 28;

        then

         A10: A1 misses ( Cl A2);

        (( Cl A1) /\ A2) c= A2 by XBOOLE_1: 17;

        then (( Cl A1) /\ A2) = {} by A2, A8, XBOOLE_1: 1, XBOOLE_1: 28;

        then ( Cl A1) misses A2;

        hence thesis by A10, CONNSP_1:def 1;

      end;

    end;

    theorem :: TSEP_2:26

    

     Th26: B1 = (the carrier of X0 /\ A1) & B2 = (the carrier of X0 /\ A2) implies ((A1,A2) are_separated implies (B1,B2) are_separated )

    proof

      assume

       A1: B1 = (the carrier of X0 /\ A1);

      then

      reconsider C1 = B1 as Subset of X;

      assume

       A2: B2 = (the carrier of X0 /\ A2);

      then

       A3: B2 c= A2 by XBOOLE_1: 17;

      reconsider C2 = B2 as Subset of X by A2;

      assume

       A4: (A1,A2) are_separated ;

      B1 c= A1 by A1, XBOOLE_1: 17;

      then (C1,C2) are_separated by A3, A4, CONNSP_1: 7;

      hence thesis by Th25;

    end;

    theorem :: TSEP_2:27

    

     Th27: B1 = A1 & B2 = A2 implies ((A1,A2) are_weakly_separated iff (B1,B2) are_weakly_separated ) by Th25;

    theorem :: TSEP_2:28

    

     Th28: B1 = (the carrier of X0 /\ A1) & B2 = (the carrier of X0 /\ A2) implies ((A1,A2) are_weakly_separated implies (B1,B2) are_weakly_separated )

    proof

      assume B1 = (the carrier of X0 /\ A1) & B2 = (the carrier of X0 /\ A2);

      then

       A1: (B1 \ B2) = (the carrier of X0 /\ (A1 \ A2)) & (B2 \ B1) = (the carrier of X0 /\ (A2 \ A1)) by XBOOLE_1: 50;

      assume ((A1 \ A2),(A2 \ A1)) are_separated ;

      then ((B1 \ B2),(B2 \ B1)) are_separated by A1, Th26;

      hence thesis;

    end;

    begin

    definition

      let X be non empty TopSpace, X1,X2 be SubSpace of X;

      :: TSEP_2:def2

      pred X1,X2 constitute_a_decomposition means for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) constitute_a_decomposition ;

      symmetry ;

    end

    notation

      let X be non empty TopSpace, X1,X2 be SubSpace of X;

      antonym X1,X2 do_not_constitute_a_decomposition for X1,X2 constitute_a_decomposition ;

    end

    reserve X0,X1,X2,Y1,Y2 for non empty SubSpace of X;

    theorem :: TSEP_2:29

    

     Th29: (X1,X2) constitute_a_decomposition iff X1 misses X2 & the TopStruct of X = (X1 union X2)

    proof

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      thus (X1,X2) constitute_a_decomposition implies X1 misses X2 & the TopStruct of X = (X1 union X2)

      proof

        assume for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) constitute_a_decomposition ;

        then

         A1: (A1,A2) constitute_a_decomposition ;

        then A1 misses A2;

        hence X1 misses X2;

        (A1 \/ A2) = the carrier of X by A1;

        then

         A2: the carrier of (X1 union X2) = the carrier of X by TSEP_1:def 2;

        X is SubSpace of X by TSEP_1: 2;

        hence thesis by A2, TSEP_1: 5;

      end;

      assume

       A3: X1 misses X2;

      assume the TopStruct of X = (X1 union X2);

      then for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) constitute_a_decomposition by A3, TSEP_1:def 2;

      hence thesis;

    end;

    theorem :: TSEP_2:30

    

     Th30: (X0,X0) do_not_constitute_a_decomposition

    proof

      reconsider A0 = the carrier of X0 as Subset of X by TSEP_1: 1;

      now

        take A1 = A0, A2 = A0;

        thus A1 = the carrier of X0 & A2 = the carrier of X0 & (A1,A2) do_not_constitute_a_decomposition by Th7;

      end;

      hence thesis;

    end;

    definition

      let X be non empty TopSpace, A1,A2 be non empty SubSpace of X;

      :: original: constitute_a_decomposition

      redefine

      pred A1,A2 constitute_a_decomposition ;

      irreflexivity by Th30;

    end

    theorem :: TSEP_2:31

    (X1,X0) constitute_a_decomposition & (X0,X2) constitute_a_decomposition implies the TopStruct of X1 = the TopStruct of X2

    proof

      reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume for A1,A0 be Subset of X st A1 = the carrier of X1 & A0 = the carrier of X0 holds (A1,A0) constitute_a_decomposition ;

      then

       A1: (A1,A0) constitute_a_decomposition ;

      assume for A0,A2 be Subset of X st A0 = the carrier of X0 & A2 = the carrier of X2 holds (A0,A2) constitute_a_decomposition ;

      then (A0,A2) constitute_a_decomposition ;

      hence thesis by A1, Th8, TSEP_1: 5;

    end;

    theorem :: TSEP_2:32

    

     Th32: for X1,X2,Y1,Y2 be non empty SubSpace of X st (X1,Y1) constitute_a_decomposition & (X2,Y2) constitute_a_decomposition holds (Y1 union Y2) = the TopStruct of X iff X1 misses X2

    proof

      let X1,X2,Y1,Y2 be non empty SubSpace of X;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      assume that

       A1: (X1,Y1) constitute_a_decomposition and

       A2: (X2,Y2) constitute_a_decomposition ;

      

       A3: (A2,B2) constitute_a_decomposition by A2;

      then

       A4: A2 = (B2 ` ) by Th3;

      

       A5: A2 = (B2 ` ) by A3, Th3;

      

       A6: (A1,B1) constitute_a_decomposition by A1;

      then

       A7: A1 = (B1 ` ) by Th3;

      thus (Y1 union Y2) = the TopStruct of X implies X1 misses X2

      proof

        assume (Y1 union Y2) = the TopStruct of X;

        then (B1 \/ B2) = the carrier of X by TSEP_1:def 2;

        then ((B1 \/ B2) ` ) = ( {} X) by XBOOLE_1: 37;

        then (A1 /\ A2) = {} by A7, A5, XBOOLE_1: 53;

        then A1 misses A2;

        hence thesis;

      end;

      assume X1 misses X2;

      then A1 misses A2;

      then

       A8: (A1 /\ A2) = ( {} X);

      A1 = (B1 ` ) by A6, Th3;

      then ((B1 \/ B2) ` ) = ( {} X) by A4, A8, XBOOLE_1: 53;

      then (B1 \/ B2) = (( {} X) ` );

      then

       A9: the carrier of (Y1 union Y2) = the carrier of X by TSEP_1:def 2;

      X is SubSpace of X by TSEP_1: 2;

      hence thesis by A9, TSEP_1: 5;

    end;

    theorem :: TSEP_2:33

    

     Th33: (X1,X2) constitute_a_decomposition implies (X1 is open iff X2 is closed)

    proof

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) constitute_a_decomposition ;

      thus X1 is open implies X2 is closed

      proof

        assume

         A2: for A1 be Subset of X st A1 = the carrier of X1 holds A1 is open;

        now

          let A2 be Subset of X;

          assume A2 = the carrier of X2;

          then

           A3: (A1,A2) constitute_a_decomposition by A1;

          A1 is open by A2;

          hence A2 is closed by A3, Th11;

        end;

        hence thesis;

      end;

      assume

       A4: for A2 be Subset of X st A2 = the carrier of X2 holds A2 is closed;

      now

        let A1 be Subset of X;

        assume A1 = the carrier of X1;

        then

         A5: (A1,A2) constitute_a_decomposition by A1;

        A2 is closed by A4;

        hence A1 is open by A5, Th11;

      end;

      hence thesis;

    end;

    theorem :: TSEP_2:34

    (X1,X2) constitute_a_decomposition implies (X1 is closed iff X2 is open) by Th33;

    theorem :: TSEP_2:35

    

     Th35: X1 meets Y1 & (X1,X2) constitute_a_decomposition & (Y1,Y2) constitute_a_decomposition implies ((X1 meet Y1),(X2 union Y2)) constitute_a_decomposition

    proof

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      assume

       A1: X1 meets Y1;

      assume for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) constitute_a_decomposition ;

      then

       A2: (A1,A2) constitute_a_decomposition ;

      assume for B1,B2 be Subset of X st B1 = the carrier of Y1 & B2 = the carrier of Y2 holds (B1,B2) constitute_a_decomposition ;

      then

       A3: (B1,B2) constitute_a_decomposition ;

      now

        let C,D be Subset of X;

        assume C = the carrier of (X1 meet Y1) & D = the carrier of (X2 union Y2);

        then C = (A1 /\ B1) & D = (A2 \/ B2) by A1, TSEP_1:def 2, TSEP_1:def 4;

        hence (C,D) constitute_a_decomposition by A2, A3, Th13;

      end;

      hence thesis;

    end;

    theorem :: TSEP_2:36

    X2 meets Y2 & (X1,X2) constitute_a_decomposition & (Y1,Y2) constitute_a_decomposition implies ((X1 union Y1),(X2 meet Y2)) constitute_a_decomposition by Th35;

    begin

    reserve X for non empty TopSpace;

    theorem :: TSEP_2:37

    

     Th37: for X1,X2,Y1,Y2 be SubSpace of X st (X1,Y1) constitute_a_decomposition & (X2,Y2) constitute_a_decomposition holds (X1,X2) are_weakly_separated implies (Y1,Y2) are_weakly_separated

    proof

      let X1,X2,Y1,Y2 be SubSpace of X;

      assume

       A1: for A1,B1 be Subset of X st A1 = the carrier of X1 & B1 = the carrier of Y1 holds (A1,B1) constitute_a_decomposition ;

      assume

       A2: for A2,B2 be Subset of X st A2 = the carrier of X2 & B2 = the carrier of Y2 holds (A2,B2) constitute_a_decomposition ;

      assume

       A3: for A1,A2 be Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds (A1,A2) are_weakly_separated ;

      now

        reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

        let B1,B2 be Subset of X;

        assume B1 = the carrier of Y1 & B2 = the carrier of Y2;

        then

         A4: (A1,B1) constitute_a_decomposition & (A2,B2) constitute_a_decomposition by A1, A2;

        (A1,A2) are_weakly_separated by A3;

        hence (B1,B2) are_weakly_separated by A4, Th15;

      end;

      hence thesis;

    end;

    theorem :: TSEP_2:38

    for X1,X2,Y1,Y2 be non empty SubSpace of X st (X1,Y1) constitute_a_decomposition & (X2,Y2) constitute_a_decomposition holds (X1,X2) are_separated implies (Y1,Y2) are_weakly_separated by TSEP_1: 78, Th37;

    theorem :: TSEP_2:39

    

     Th39: for X1,X2,Y1,Y2 be non empty SubSpace of X st (X1,Y1) constitute_a_decomposition & (X2,Y2) constitute_a_decomposition holds X1 misses X2 & (Y1,Y2) are_weakly_separated implies (X1,X2) are_separated by Th37, TSEP_1: 78;

    theorem :: TSEP_2:40

    for X1,X2,Y1,Y2 be non empty SubSpace of X st (X1,Y1) constitute_a_decomposition & (X2,Y2) constitute_a_decomposition holds (Y1 union Y2) = the TopStruct of X & (Y1,Y2) are_weakly_separated implies (X1,X2) are_separated

    proof

      let X1,X2,Y1,Y2 be non empty SubSpace of X;

      assume

       A1: (X1,Y1) constitute_a_decomposition & (X2,Y2) constitute_a_decomposition ;

      assume (Y1 union Y2) = the TopStruct of X;

      then

       A2: X1 misses X2 by A1, Th32;

      assume (Y1,Y2) are_weakly_separated ;

      hence thesis by A1, A2, Th39;

    end;

    theorem :: TSEP_2:41

    for X1,X2 be non empty SubSpace of X st (X1,X2) constitute_a_decomposition holds ((X1,X2) are_weakly_separated iff (X1,X2) are_separated ) by Th29, TSEP_1: 78;

    theorem :: TSEP_2:42

    for X1,X2,Y1,Y2 be non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (Y1 union Y2) = (X1 union X2) holds (Y1,Y2) are_weakly_separated implies (X1,X2) are_weakly_separated

    proof

      let X1,X2,Y1,Y2 be non empty SubSpace of X;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;

      then

       A1: C1 c= A1 & C2 c= A2 by TSEP_1: 4;

      assume

       A2: (Y1 union Y2) = (X1 union X2);

      assume (Y1,Y2) are_weakly_separated ;

      then

       A3: (C1,C2) are_weakly_separated ;

      now

        let A1,A2 be Subset of X;

        assume

         A4: A1 = the carrier of X1 & A2 = the carrier of X2;

        then (A1 \/ A2) = the carrier of (X1 union X2) by TSEP_1:def 2;

        then (A1 \/ A2) = (C1 \/ C2) by A2, TSEP_1:def 2;

        hence (A1,A2) are_weakly_separated by A1, A3, A4, Th22;

      end;

      hence thesis;

    end;

    theorem :: TSEP_2:43

    for X1,X2,Y1,Y2 be non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & (Y1 meet Y2) = (X1 meet X2) holds (X1,X2) are_weakly_separated implies (Y1,Y2) are_weakly_separated

    proof

      let X1,X2,Y1,Y2 be non empty SubSpace of X;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1: 1;

      assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;

      then

       A1: C1 c= A1 & C2 c= A2 by TSEP_1: 4;

      assume

       A2: Y1 meets Y2;

      assume

       A3: (Y1 meet Y2) = (X1 meet X2);

      assume (X1,X2) are_weakly_separated ;

      then

       A4: (A1,A2) are_weakly_separated ;

      now

        let C1,C2 be Subset of X;

        assume

         A5: C1 = the carrier of Y1 & C2 = the carrier of Y2;

        then C1 meets C2 by A2;

        then (C1 /\ C2) <> {} ;

        then (A1 /\ A2) <> {} by A1, A5, XBOOLE_1: 3, XBOOLE_1: 27;

        then A1 meets A2;

        then X1 meets X2;

        then (A1 /\ A2) = the carrier of (X1 meet X2) by TSEP_1:def 4;

        then (A1 /\ A2) = (C1 /\ C2) by A2, A3, A5, TSEP_1:def 4;

        hence (C1,C2) are_weakly_separated by A1, A4, A5, Th24;

      end;

      hence thesis;

    end;

    reserve X0 for non empty SubSpace of X;

    theorem :: TSEP_2:44

    

     Th44: for X1,X2 be SubSpace of X, Y1,Y2 be SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds (X1,X2) are_separated iff (Y1,Y2) are_separated

    proof

      let X1,X2 be SubSpace of X, X01,X02 be SubSpace of X0;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider B1 = the carrier of X01, B2 = the carrier of X02 as Subset of X0 by TSEP_1: 1;

      assume

       A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02;

      thus (X1,X2) are_separated implies (X01,X02) are_separated

      proof

        assume (X1,X2) are_separated ;

        then (A1,A2) are_separated ;

        then for B1,B2 be Subset of X0 holds B1 = the carrier of X01 & B2 = the carrier of X02 implies (B1,B2) are_separated by A1, Th25;

        hence thesis;

      end;

      thus (X01,X02) are_separated implies (X1,X2) are_separated

      proof

        assume (X01,X02) are_separated ;

        then (B1,B2) are_separated ;

        then for A1,A2 be Subset of X holds A1 = the carrier of X1 & A2 = the carrier of X2 implies (A1,A2) are_separated by A1, Th25;

        hence thesis;

      end;

    end;

    theorem :: TSEP_2:45

    for X1,X2 be non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds for Y1,Y2 be SubSpace of X0 st Y1 = (X1 meet X0) & Y2 = (X2 meet X0) holds (X1,X2) are_separated implies (Y1,Y2) are_separated

    proof

      let X1,X2 be non empty SubSpace of X;

      assume

       A1: X1 meets X0 & X2 meets X0;

      let Y1,Y2 be SubSpace of X0;

      assume

       A2: Y1 = (X1 meet X0) & Y2 = (X2 meet X0);

      assume (X1,X2) are_separated ;

      then ((X1 meet X0),(X2 meet X0)) are_separated by A1, TSEP_1: 70;

      hence thesis by A2, Th44;

    end;

    theorem :: TSEP_2:46

    for X1,X2 be SubSpace of X, Y1,Y2 be SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds (X1,X2) are_weakly_separated iff (Y1,Y2) are_weakly_separated

    proof

      let X1,X2 be SubSpace of X, X01,X02 be SubSpace of X0;

      reconsider A1 = the carrier of X1 as Subset of X by TSEP_1: 1;

      reconsider A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      reconsider B1 = the carrier of X01 as Subset of X0 by TSEP_1: 1;

      reconsider B2 = the carrier of X02 as Subset of X0 by TSEP_1: 1;

      assume

       A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the carrier of X02;

      thus (X1,X2) are_weakly_separated implies (X01,X02) are_weakly_separated

      proof

        assume (X1,X2) are_weakly_separated ;

        then (A1,A2) are_weakly_separated ;

        then for B1,B2 be Subset of X0 holds B1 = the carrier of X01 & B2 = the carrier of X02 implies (B1,B2) are_weakly_separated by A1, Th27;

        hence thesis;

      end;

      thus (X01,X02) are_weakly_separated implies (X1,X2) are_weakly_separated

      proof

        assume (X01,X02) are_weakly_separated ;

        then (B1,B2) are_weakly_separated ;

        then for A1,A2 be Subset of X holds A1 = the carrier of X1 & A2 = the carrier of X2 implies (A1,A2) are_weakly_separated by A1, Th27;

        hence thesis;

      end;

    end;

    theorem :: TSEP_2:47

    for X1,X2 be non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds for Y1,Y2 be SubSpace of X0 st Y1 = (X1 meet X0) & Y2 = (X2 meet X0) holds (X1,X2) are_weakly_separated implies (Y1,Y2) are_weakly_separated

    proof

      let X1,X2 be non empty SubSpace of X;

      reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1: 1;

      assume

       A1: X1 meets X0 & X2 meets X0;

      let Y1,Y2 be SubSpace of X0;

      assume

       A2: Y1 = (X1 meet X0) & Y2 = (X2 meet X0);

      assume (X1,X2) are_weakly_separated ;

      then

       A3: (A1,A2) are_weakly_separated ;

      now

        let C1,C2 be Subset of X0;

        assume C1 = the carrier of Y1 & C2 = the carrier of Y2;

        then C1 = (the carrier of X0 /\ A1) & C2 = (the carrier of X0 /\ A2) by A1, A2, TSEP_1:def 4;

        hence (C1,C2) are_weakly_separated by A3, Th28;

      end;

      hence thesis;

    end;