tsep_1.miz

    begin



     Lm1: for A be set holds for B,C,D be Subset of A st (B \ C) = {} holds B misses (D \ C)

    proof

      let A be set;

      let B,C,D be Subset of A;

      assume (B \ C) = {} ;

      then

       A1: B c= C by XBOOLE_1: 37;

      C misses (D \ C) by XBOOLE_1: 79;

      hence thesis by A1, XBOOLE_1: 63;

    end;



     Lm2: for A,B,C be set holds ((A /\ B) \ C) = ((A \ C) /\ (B \ C))

    proof

      let A,B,C be set;



       A1: (A \ C) misses C by XBOOLE_1: 79;



      thus ((A /\ B) \ C) = ((A \ C) /\ B) by XBOOLE_1: 49

      .= ((A \ C) \ ((A \ C) \ B)) by XBOOLE_1: 48

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

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

      .= ( {} \/ ((A \ C) /\ (C \/ B))) by XBOOLE_1: 37

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

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

      .= (((A \ C) /\ (B \ C)) \/ {} ) by A1, XBOOLE_0:def 7

      .= ((A \ C) /\ (B \ C));

    end;

    reserve X for TopSpace;

    theorem :: TSEP_1:1



     Th1: for X be TopStruct, X0 be SubSpace of X holds the carrier of X0 is Subset of X

    proof

      let X be TopStruct, X0 be SubSpace of X;

      reconsider A = ( [#] X0) as Subset of ( [#] X) by PRE_TOPC:def 4;

      A c= ( [#] X);

      hence thesis;

    end;

    theorem :: TSEP_1:2



     Th2: for X be TopStruct holds X is SubSpace of X

    proof

      let X be TopStruct;

      thus ( [#] X) c= ( [#] X);

      thus for P be Subset of X holds P in the topology of X iff ex Q be Subset of X st Q in the topology of X & P = (Q /\ ( [#] X))

      proof

        let P be Subset of X;

        thus P in the topology of X implies ex Q be Subset of X st Q in the topology of X & P = (Q /\ ( [#] X))

        proof

          assume

           A1: P in the topology of X;

          take P;

          thus thesis by A1, XBOOLE_1: 28;

        end;

        thus thesis by XBOOLE_1: 28;

      end;

    end;

    theorem :: TSEP_1:3

    for X be strict TopStruct holds (X | ( [#] X)) = X

    proof

      let X be strict TopStruct;

      reconsider X0 = X as SubSpace of X by Th2;

      reconsider P = ( [#] X0) as Subset of X;

      (X | P) = X0 by PRE_TOPC:def 5;

      hence thesis;

    end;

    theorem :: TSEP_1:4



     Th4: for X1,X2 be SubSpace of X holds the carrier of X1 c= the carrier of X2 iff X1 is SubSpace of X2

    proof

      let X1,X2 be SubSpace of X;

      set A1 = the carrier of X1, A2 = the carrier of X2;



       A1: A1 = ( [#] X1);



       A2: A2 = ( [#] X2);

      thus the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2

      proof

        assume

         A3: A1 c= A2;

        for P be Subset of X1 holds P in the topology of X1 iff ex Q be Subset of X2 st Q in the topology of X2 & P = (Q /\ A1)

        proof

          let P be Subset of X1;

          thus P in the topology of X1 implies ex Q be Subset of X2 st Q in the topology of X2 & P = (Q /\ A1)

          proof

            assume P in the topology of X1;

            then

            consider R be Subset of X such that

             A4: R in the topology of X and

             A5: P = (R /\ A1) by A1, PRE_TOPC:def 4;

            reconsider Q = (R /\ A2) as Subset of X2 by XBOOLE_1: 17;

            take Q;

            thus Q in the topology of X2 by A2, A4, PRE_TOPC:def 4;

            (Q /\ A1) = (R /\ (A2 /\ A1)) by XBOOLE_1: 16

            .= (R /\ A1) by A3, XBOOLE_1: 28;

            hence thesis by A5;

          end;

          given Q be Subset of X2 such that

           A6: Q in the topology of X2 and

           A7: P = (Q /\ A1);

          consider R be Subset of X such that

           A8: R in the topology of X and

           A9: Q = (R /\ ( [#] X2)) by A6, PRE_TOPC:def 4;

          P = (R /\ (A2 /\ A1)) by A7, A9, XBOOLE_1: 16

          .= (R /\ A1) by A3, XBOOLE_1: 28;

          hence thesis by A1, A8, PRE_TOPC:def 4;

        end;

        hence thesis by A1, A2, A3, PRE_TOPC:def 4;

      end;

      thus thesis by A1, A2, PRE_TOPC:def 4;

    end;



     Lm3: for X be TopStruct, X0 be SubSpace of X holds the TopStruct of X0 is strict SubSpace of X

    proof

      let X be TopStruct, X0 be SubSpace of X;

      set S = the TopStruct of X0;

      S is SubSpace of X

      proof



         A1: ( [#] X0) = the carrier of X0;

        hence ( [#] S) c= ( [#] X) by PRE_TOPC:def 4;

        let P be Subset of S;

        thus P in the topology of S implies ex Q be Subset of X st Q in the topology of X & P = (Q /\ ( [#] S)) by A1, PRE_TOPC:def 4;

        given Q be Subset of X such that

         A2: Q in the topology of X & P = (Q /\ ( [#] S));

        thus thesis by A1, A2, PRE_TOPC:def 4;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:5



     Th5: for X be TopStruct holds for X1,X2 be SubSpace of X st the carrier of X1 = the carrier of X2 holds the TopStruct of X1 = the TopStruct of X2

    proof

      let X be TopStruct;

      let X1,X2 be SubSpace of X;

      reconsider S1 = the TopStruct of X1, S2 = the TopStruct of X2 as strict SubSpace of X by Lm3;

      set A1 = the carrier of X1, A2 = the carrier of X2;

      assume

       A1: A1 = A2;



       A2: A1 = ( [#] S1);



       A3: A2 = ( [#] S2);

      reconsider A1 as Subset of X by BORSUK_1: 1;

      S1 = (X | A1) by A2, PRE_TOPC:def 5;

      hence thesis by A1, A3, PRE_TOPC:def 5;

    end;

    theorem :: TSEP_1:6

    for X1,X2 be SubSpace of X st X1 is SubSpace of X2 & X2 is SubSpace of X1 holds the TopStruct of X1 = the TopStruct of X2

    proof

      let X1,X2 be SubSpace of X;

      set A1 = the carrier of X1, A2 = the carrier of X2;

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

      then A1 c= A2 & A2 c= A1 by Th4;

      then A1 = A2 by XBOOLE_0:def 10;

      hence thesis by Th5;

    end;

    theorem :: TSEP_1:7



     Th7: for X1 be SubSpace of X holds for X2 be SubSpace of X1 holds X2 is SubSpace of X

    proof

      let X1 be SubSpace of X;

      let X2 be SubSpace of X1;



       A1: ( [#] X2) c= ( [#] X1) by PRE_TOPC:def 4;

      ( [#] X1) c= ( [#] X) by PRE_TOPC:def 4;

      hence ( [#] X2) c= ( [#] X) by A1, XBOOLE_1: 1;

      thus for P be Subset of X2 holds P in the topology of X2 iff ex Q be Subset of X st Q in the topology of X & P = (Q /\ ( [#] X2))

      proof

        let P be Subset of X2;

        reconsider P1 = P as Subset of X2;

        thus P in the topology of X2 implies ex Q be Subset of X st Q in the topology of X & P = (Q /\ ( [#] X2))

        proof

          assume P in the topology of X2;

          then

          consider R be Subset of X1 such that

           A2: R in the topology of X1 and

           A3: P = (R /\ ( [#] X2)) by PRE_TOPC:def 4;

          consider Q be Subset of X such that

           A4: Q in the topology of X and

           A5: R = (Q /\ ( [#] X1)) by A2, PRE_TOPC:def 4;

          (Q /\ ( [#] X2)) = (Q /\ (( [#] X1) /\ ( [#] X2))) by A1, XBOOLE_1: 28

          .= P by A3, A5, XBOOLE_1: 16;

          hence thesis by A4;

        end;

        given Q be Subset of X such that

         A6: Q in the topology of X and

         A7: P = (Q /\ ( [#] X2));

        reconsider R = (Q /\ ( [#] X1)) as Subset of X1;

        reconsider Q1 = Q as Subset of X;

        Q1 is open by A6;

        then

         A8: R is open by TOPS_2: 24;

        (R /\ ( [#] X2)) = (Q /\ (( [#] X1) /\ ( [#] X2))) by XBOOLE_1: 16

        .= P by A1, A7, XBOOLE_1: 28;

        then P1 is open by A8, TOPS_2: 24;

        hence thesis;

      end;

    end;

    theorem :: TSEP_1:8



     Th8: for X0 be SubSpace of X, C,A be Subset of X, B be Subset of X0 st C is closed & C c= the carrier of X0 & A c= C & A = B holds B is closed iff A is closed

    proof

      let X0 be SubSpace of X, C,A be Subset of X, B be Subset of X0 such that

       A1: C is closed and

       A2: C c= the carrier of X0 and

       A3: A c= C and

       A4: A = B;

      thus B is closed implies A is closed

      proof

        assume B is closed;

        then

        consider F be Subset of X such that

         A5: F is closed and

         A6: (F /\ ( [#] X0)) = B by PRE_TOPC: 13;

        A c= F by A4, A6, XBOOLE_1: 17;

        then

         A7: A c= (F /\ C) by A3, XBOOLE_1: 19;

        (F /\ C) c= A by A2, A4, A6, XBOOLE_1: 26;

        hence thesis by A1, A5, A7, XBOOLE_0:def 10;

      end;

      thus thesis by A4, TOPS_2: 26;

    end;

    theorem :: TSEP_1:9



     Th9: for X0 be SubSpace of X, C,A be Subset of X, B be Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds B is open iff A is open

    proof

      let X0 be SubSpace of X, C,A be Subset of X, B be Subset of X0 such that

       A1: C is open and

       A2: C c= the carrier of X0 and

       A3: A c= C and

       A4: A = B;

      thus B is open implies A is open

      proof

        assume B is open;

        then

        consider F be Subset of X such that

         A5: F is open and

         A6: (F /\ ( [#] X0)) = B by TOPS_2: 24;

        A c= F by A4, A6, XBOOLE_1: 17;

        then

         A7: A c= (F /\ C) by A3, XBOOLE_1: 19;

        (F /\ C) c= A by A2, A4, A6, XBOOLE_1: 26;

        hence thesis by A1, A5, A7, XBOOLE_0:def 10;

      end;

      thus thesis by A4, TOPS_2: 25;

    end;

    theorem :: TSEP_1:10



     Th10: for X be non empty TopStruct, A0 be non empty Subset of X holds ex X0 be strict non empty SubSpace of X st A0 = the carrier of X0

    proof

      let X be non empty TopStruct, A0 be non empty Subset of X;

      take X0 = (X | A0);

      A0 = ( [#] X0) by PRE_TOPC:def 5;

      hence thesis;

    end;

    theorem :: TSEP_1:11



     Th11: for X0 be SubSpace of X, A be Subset of X st A = the carrier of X0 holds X0 is closed SubSpace of X iff A is closed

    proof

      let X0 be SubSpace of X, A be Subset of X;

      assume

       A1: A = the carrier of X0;

      hence X0 is closed SubSpace of X implies A is closed by BORSUK_1:def 11;

      thus A is closed implies X0 is closed SubSpace of X

      proof

        assume A is closed;

        then for B be Subset of X holds B = the carrier of X0 implies B is closed by A1;

        hence thesis by BORSUK_1:def 11;

      end;

    end;

    theorem :: TSEP_1:12

    for X0 be closed SubSpace of X, A be Subset of X, B be Subset of X0 st A = B holds B is closed iff A is closed

    proof

      let X0 be closed SubSpace of X, A be Subset of X, B be Subset of X0 such that

       A1: A = B;

      reconsider C = the carrier of X0 as Subset of X by Th1;

      C is closed by Th11;

      hence thesis by A1, Th8;

    end;

    theorem :: TSEP_1:13

    for X1 be closed SubSpace of X, X2 be closed SubSpace of X1 holds X2 is closed SubSpace of X

    proof

      let X1 be closed SubSpace of X, X2 be closed SubSpace of X1;

      now

        reconsider C = ( [#] X1) as Subset of X by BORSUK_1: 1;

        let B be Subset of X;

        assume

         A1: B = the carrier of X2;

        then

        reconsider BB = B as Subset of X1 by BORSUK_1: 1;

        BB is closed by A1, BORSUK_1:def 11;

        then

         A2: ex A be Subset of X st A is closed & (A /\ ( [#] X1)) = BB by PRE_TOPC: 13;

        C is closed by BORSUK_1:def 11;

        hence B is closed by A2;

      end;

      hence thesis by Th7, BORSUK_1:def 11;

    end;

    theorem :: TSEP_1:14

    for X be non empty TopSpace, X1 be closed non empty SubSpace of X, X2 be non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds X1 is closed non empty SubSpace of X2

    proof

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

      assume the carrier of X1 c= the carrier of X2;

      then

      reconsider B = the carrier of X1 as Subset of X2;

      now

        let C be Subset of X2;

        assume

         A1: C = the carrier of X1;

        then

        reconsider A = C as Subset of X by BORSUK_1: 1;



         A2: (A /\ ( [#] X2)) = C by XBOOLE_1: 28;

        A is closed by A1, Th11;

        hence C is closed by A2, PRE_TOPC: 13;

      end;

      then B is closed;

      hence thesis by Th4, Th11;

    end;

    theorem :: TSEP_1:15



     Th15: for X be non empty TopSpace, A0 be non empty Subset of X st A0 is closed holds ex X0 be strict closed non empty SubSpace of X st A0 = the carrier of X0

    proof

      let X be non empty TopSpace, A0 be non empty Subset of X such that

       A1: A0 is closed;

      consider X0 be strict non empty SubSpace of X such that

       A2: A0 = the carrier of X0 by Th10;

      reconsider Y0 = X0 as strict closed non empty SubSpace of X by A1, A2, Th11;

      take Y0;

      thus thesis by A2;

    end;

    definition

      let X be TopStruct;

      let IT be SubSpace of X;

      :: TSEP_1:def1

      attr IT is open means

      : Def1: for A be Subset of X st A = the carrier of IT holds A is open;

    end



     Lm4: for T be TopStruct holds the TopStruct of T is SubSpace of T

    proof

      let T be TopStruct;

      set S = the TopStruct of T;

      thus ( [#] S) c= ( [#] T);

      let P be Subset of S;

      hereby

        reconsider Q = P as Subset of T;

        assume

         A1: P in the topology of S;

        take Q;

        thus Q in the topology of T by A1;

        thus P = (Q /\ ( [#] S)) by XBOOLE_1: 28;

      end;

      given Q be Subset of T such that

       A2: Q in the topology of T & P = (Q /\ ( [#] S));

      thus thesis by A2, XBOOLE_1: 28;

    end;

    registration

      let X be TopSpace;

      cluster strict open for SubSpace of X;

      existence

      proof

        reconsider Y = the TopStruct of X as strict SubSpace of X by Lm4;

        take Y;

        Y is open

        proof

          let A be Subset of X;

          assume A = the carrier of Y;

          then A = ( [#] X);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let X be non empty TopSpace;

      cluster strict open non empty for SubSpace of X;

      existence

      proof

        (X | ( [#] X)) is open

        proof

          let A be Subset of X;

          assume A = the carrier of (X | ( [#] X));



          then A = ( [#] (X | ( [#] X)))

          .= ( [#] X) by PRE_TOPC:def 5;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: TSEP_1:16



     Th16: for X0 be SubSpace of X, A be Subset of X st A = the carrier of X0 holds X0 is open SubSpace of X iff A is open

    proof

      let X0 be SubSpace of X, A be Subset of X;

      assume

       A1: A = the carrier of X0;

      hence X0 is open SubSpace of X implies A is open by Def1;

      thus A is open implies X0 is open SubSpace of X

      proof

        assume A is open;

        then for B be Subset of X holds B = the carrier of X0 implies B is open by A1;

        hence thesis by Def1;

      end;

    end;

    theorem :: TSEP_1:17

    for X0 be open SubSpace of X, A be Subset of X, B be Subset of X0 st A = B holds B is open iff A is open

    proof

      let X0 be open SubSpace of X, A be Subset of X, B be Subset of X0 such that

       A1: A = B;

      reconsider C = the carrier of X0 as Subset of X by Th1;

      C is open by Th16;

      hence thesis by A1, Th9;

    end;

    theorem :: TSEP_1:18

    for X1 be open SubSpace of X, X2 be open SubSpace of X1 holds X2 is open SubSpace of X

    proof

      let X1 be open SubSpace of X, X2 be open SubSpace of X1;

      now

        reconsider C = ( [#] X1) as Subset of X by BORSUK_1: 1;

        let B be Subset of X;

        assume

         A1: B = the carrier of X2;

        then

        reconsider BB = B as Subset of X1 by BORSUK_1: 1;

        BB is open by A1, Def1;

        then

         A2: ex A be Subset of X st A is open & (A /\ ( [#] X1)) = BB by TOPS_2: 24;

        C is open by Def1;

        hence B is open by A2;

      end;

      hence thesis by Def1, Th7;

    end;

    theorem :: TSEP_1:19

    for X be non empty TopSpace, X1 be open SubSpace of X, X2 be non empty SubSpace of X st the carrier of X1 c= the carrier of X2 holds X1 is open SubSpace of X2

    proof

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

      assume the carrier of X1 c= the carrier of X2;

      then

      reconsider B = the carrier of X1 as Subset of X2;

      now

        let C be Subset of X2;

        assume

         A1: C = the carrier of X1;

        then

        reconsider A = C as Subset of X by BORSUK_1: 1;



         A2: (A /\ ( [#] X2)) = C by XBOOLE_1: 28;

        A is open by A1, Th16;

        hence C is open by A2, TOPS_2: 24;

      end;

      then B is open;

      hence thesis by Th4, Th16;

    end;

    theorem :: TSEP_1:20



     Th20: for X be non empty TopSpace, A0 be non empty Subset of X st A0 is open holds ex X0 be strict open non empty SubSpace of X st A0 = the carrier of X0

    proof

      let X be non empty TopSpace, A0 be non empty Subset of X such that

       A1: A0 is open;

      consider X0 be strict non empty SubSpace of X such that

       A2: A0 = the carrier of X0 by Th10;

      reconsider Y0 = X0 as strict open non empty SubSpace of X by A1, A2, Th16;

      take Y0;

      thus thesis by A2;

    end;

    begin

    reserve X for non empty TopSpace;

    definition

      let X be non empty TopStruct;

      let X1,X2 be non empty SubSpace of X;

      :: TSEP_1:def2

      func X1 union X2 -> strict non empty SubSpace of X means

      : Def2: the carrier of it = (the carrier of X1 \/ the carrier of X2);

      existence

      proof

        reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by Th1;

        set A = (A1 \/ A2);

        reconsider A as non empty Subset of X;

        take (X | A);



        thus the carrier of (X | A) = ( [#] (X | A))

        .= (the carrier of X1 \/ the carrier of X2) by PRE_TOPC:def 5;

      end;

      uniqueness by Th5;

      commutativity ;

    end

    reserve X1,X2,X3 for non empty SubSpace of X;

    theorem :: TSEP_1:21

    ((X1 union X2) union X3) = (X1 union (X2 union X3))

    proof

      the carrier of ((X1 union X2) union X3) = (the carrier of (X1 union X2) \/ the carrier of X3) by Def2

      .= ((the carrier of X1 \/ the carrier of X2) \/ the carrier of X3) by Def2

      .= (the carrier of X1 \/ (the carrier of X2 \/ the carrier of X3)) by XBOOLE_1: 4

      .= (the carrier of X1 \/ the carrier of (X2 union X3)) by Def2

      .= the carrier of (X1 union (X2 union X3)) by Def2;

      hence thesis by Th5;

    end;

    theorem :: TSEP_1:22



     Th22: X1 is SubSpace of (X1 union X2)

    proof

      set A1 = the carrier of X1, A2 = the carrier of X2, A = the carrier of (X1 union X2);

      A = (A1 \/ A2) by Def2;

      then A1 c= A by XBOOLE_1: 7;

      hence thesis by Th4;

    end;

    theorem :: TSEP_1:23

    for X1,X2 be non empty SubSpace of X holds X1 is SubSpace of X2 iff (X1 union X2) = the TopStruct of X2

    proof

      let X1,X2 be non empty SubSpace of X;

      set A1 = the carrier of X1, A2 = the carrier of X2;

      thus X1 is SubSpace of X2 iff (X1 union X2) = the TopStruct of X2

      proof

        thus X1 is SubSpace of X2 implies (X1 union X2) = the TopStruct of X2

        proof

          assume X1 is SubSpace of X2;

          then

           A1: (A1 \/ A2) = the carrier of the TopStruct of X2 by BORSUK_1: 1, XBOOLE_1: 12;

           the TopStruct of X2 is strict SubSpace of X by Lm3;

          hence thesis by A1, Def2;

        end;

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

        then (A1 \/ A2) = A2 by Def2;

        then A1 c= A2 by XBOOLE_1: 7;

        hence thesis by Th4;

      end;

    end;

    theorem :: TSEP_1:24

    for X1,X2 be closed non empty SubSpace of X holds (X1 union X2) is closed SubSpace of X

    proof

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

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      reconsider A = the carrier of (X1 union X2) as Subset of X by Th1;

      A1 is closed & A2 is closed by Th11;

      then (A1 \/ A2) is closed;

      then A is closed by Def2;

      hence thesis by Th11;

    end;

    theorem :: TSEP_1:25

    for X1,X2 be open non empty SubSpace of X holds (X1 union X2) is open SubSpace of X

    proof

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

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      reconsider A = the carrier of (X1 union X2) as Subset of X by Th1;

      A1 is open & A2 is open by Th16;

      then (A1 \/ A2) is open;

      then A is open by Def2;

      hence thesis by Th16;

    end;

    definition

      let X1,X2 be 1-sorted;

      :: TSEP_1:def3

      pred X1 misses X2 means the carrier of X1 misses the carrier of X2;

      correctness ;

      symmetry ;

    end

    notation

      let X1,X2 be 1-sorted;

      antonym X1 meets X2 for X1 misses X2;

    end

    definition

      let X be non empty TopStruct;

      let X1,X2 be non empty SubSpace of X;

      assume

       A1: X1 meets X2;

      :: TSEP_1:def4

      func X1 meet X2 -> strict non empty SubSpace of X means

      : Def4: the carrier of it = (the carrier of X1 /\ the carrier of X2);

      existence

      proof

        reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by Th1;

        set A = (A1 /\ A2);

        A1 meets A2 by A1;

        then

        reconsider A as non empty Subset of X by XBOOLE_0:def 7;

        take (X | A);



        thus the carrier of (X | A) = ( [#] (X | A))

        .= (the carrier of X1 /\ the carrier of X2) by PRE_TOPC:def 5;

      end;

      uniqueness by Th5;

    end

    reserve X1,X2,X3 for non empty SubSpace of X;

    theorem :: TSEP_1:26



     Th26: (X1 meets X2 implies (X1 meet X2) = (X2 meet X1)) & ((X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3)) implies ((X1 meet X2) meet X3) = (X1 meet (X2 meet X3)))

    proof

      thus X1 meets X2 implies (X1 meet X2) = (X2 meet X1)

      proof

        assume

         A1: X1 meets X2;



        then the carrier of (X1 meet X2) = (the carrier of X2 /\ the carrier of X1) by Def4

        .= the carrier of (X2 meet X1) by A1, Def4;

        hence thesis by Th5;

      end;

      now

         A2:

        now

          assume that

           A3: X1 meets X2 and

           A4: (X1 meet X2) meets X3;

          the carrier of (X1 meet X2) meets the carrier of X3 by A4;

          then (the carrier of (X1 meet X2) /\ the carrier of X3) <> {} by XBOOLE_0:def 7;

          then ((the carrier of X1 /\ the carrier of X2) /\ the carrier of X3) <> {} by A3, Def4;

          then

           A5: (the carrier of X1 /\ (the carrier of X2 /\ the carrier of X3)) <> {} by XBOOLE_1: 16;

          then (the carrier of X2 /\ the carrier of X3) <> {} ;

          then

           A6: the carrier of X2 meets the carrier of X3 by XBOOLE_0:def 7;

          then X2 meets X3;

          then (the carrier of X1 /\ the carrier of (X2 meet X3)) <> {} by A5, Def4;

          then the carrier of X1 meets the carrier of (X2 meet X3) by XBOOLE_0:def 7;

          hence X1 meets X2 & (X1 meet X2) meets X3 & X2 meets X3 & X1 meets (X2 meet X3) by A3, A4, A6;

        end;

        assume

         A7: X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3);

         A8:

        now

          assume that

           A9: X2 meets X3 and

           A10: X1 meets (X2 meet X3);

          the carrier of X1 meets the carrier of (X2 meet X3) by A10;

          then (the carrier of X1 /\ the carrier of (X2 meet X3)) <> {} by XBOOLE_0:def 7;

          then (the carrier of X1 /\ (the carrier of X2 /\ the carrier of X3)) <> {} by A9, Def4;

          then

           A11: ((the carrier of X1 /\ the carrier of X2) /\ the carrier of X3) <> {} by XBOOLE_1: 16;

          then (the carrier of X1 /\ the carrier of X2) <> {} ;

          then

           A12: the carrier of X1 meets the carrier of X2 by XBOOLE_0:def 7;

          then X1 meets X2;

          then (the carrier of (X1 meet X2) /\ the carrier of X3) <> {} by A11, Def4;

          then the carrier of (X1 meet X2) meets the carrier of X3 by XBOOLE_0:def 7;

          hence X1 meets X2 & (X1 meet X2) meets X3 & X2 meets X3 & X1 meets (X2 meet X3) by A9, A10, A12;

        end;



        then the carrier of ((X1 meet X2) meet X3) = (the carrier of (X1 meet X2) /\ the carrier of X3) by A7, Def4

        .= ((the carrier of X1 /\ the carrier of X2) /\ the carrier of X3) by A7, A8, Def4

        .= (the carrier of X1 /\ (the carrier of X2 /\ the carrier of X3)) by XBOOLE_1: 16

        .= (the carrier of X1 /\ the carrier of (X2 meet X3)) by A7, A2, Def4

        .= the carrier of (X1 meet (X2 meet X3)) by A7, A2, Def4;

        hence ((X1 meet X2) meet X3) = (X1 meet (X2 meet X3)) by Th5;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:27



     Th27: X1 meets X2 implies (X1 meet X2) is SubSpace of X1 & (X1 meet X2) is SubSpace of X2

    proof

      assume X1 meets X2;

      then the carrier of (X1 meet X2) = (the carrier of X1 /\ the carrier of X2) by Def4;

      then the carrier of (X1 meet X2) c= the carrier of X1 & the carrier of (X1 meet X2) c= the carrier of X2 by XBOOLE_1: 17;

      hence thesis by Th4;

    end;

    theorem :: TSEP_1:28

    for X1,X2 be non empty SubSpace of X holds X1 meets X2 implies (X1 is SubSpace of X2 iff (X1 meet X2) = the TopStruct of X1) & (X2 is SubSpace of X1 iff (X1 meet X2) = the TopStruct of X2)

    proof

      let X1,X2 be non empty SubSpace of X;

      set A1 = the carrier of X1, A2 = the carrier of X2;

      assume

       A1: X1 meets X2;

      thus X1 is SubSpace of X2 iff (X1 meet X2) = the TopStruct of X1

      proof

        thus X1 is SubSpace of X2 implies (X1 meet X2) = the TopStruct of X1

        proof

          assume X1 is SubSpace of X2;

          then

           A2: (A1 /\ A2) = the carrier of the TopStruct of X1 by BORSUK_1: 1, XBOOLE_1: 28;

           the TopStruct of X1 is strict SubSpace of X by Lm3;

          hence thesis by A1, A2, Def4;

        end;

        assume (X1 meet X2) = the TopStruct of X1;

        then (A1 /\ A2) = A1 by A1, Def4;

        then A1 c= A2 by XBOOLE_1: 17;

        hence thesis by Th4;

      end;

      thus X2 is SubSpace of X1 iff (X1 meet X2) = the TopStruct of X2

      proof

        thus X2 is SubSpace of X1 implies (X1 meet X2) = the TopStruct of X2

        proof

          assume X2 is SubSpace of X1;

          then

           A3: (A1 /\ A2) = the carrier of the TopStruct of X2 by BORSUK_1: 1, XBOOLE_1: 28;

           the TopStruct of X2 is strict SubSpace of X by Lm3;

          hence thesis by A1, A3, Def4;

        end;

        assume (X1 meet X2) = the TopStruct of X2;

        then (A1 /\ A2) = A2 by A1, Def4;

        then A2 c= A1 by XBOOLE_1: 17;

        hence thesis by Th4;

      end;

    end;

    theorem :: TSEP_1:29

    for X1,X2 be closed non empty SubSpace of X st X1 meets X2 holds (X1 meet X2) is closed SubSpace of X

    proof

      let X1,X2 be closed non empty SubSpace of X such that

       A1: X1 meets X2;

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      reconsider A = the carrier of (X1 meet X2) as Subset of X by Th1;

      A1 is closed & A2 is closed by Th11;

      then (A1 /\ A2) is closed;

      then A is closed by A1, Def4;

      hence thesis by Th11;

    end;

    theorem :: TSEP_1:30

    for X1,X2 be open non empty SubSpace of X st X1 meets X2 holds (X1 meet X2) is open SubSpace of X

    proof

      let X1,X2 be open non empty SubSpace of X such that

       A1: X1 meets X2;

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      reconsider A = the carrier of (X1 meet X2) as Subset of X by Th1;

      A1 is open & A2 is open by Th16;

      then (A1 /\ A2) is open;

      then A is open by A1, Def4;

      hence thesis by Th16;

    end;

    theorem :: TSEP_1:31

    X1 meets X2 implies (X1 meet X2) is SubSpace of (X1 union X2)

    proof

      assume X1 meets X2;

      then

       A1: (X1 meet X2) is SubSpace of X1 by Th27;

      X1 is SubSpace of (X1 union X2) by Th22;

      hence thesis by A1, Th7;

    end;

    theorem :: TSEP_1:32

    for Y be non empty SubSpace of X st X1 meets Y & Y meets X2 holds ((X1 union X2) meet Y) = ((X1 meet Y) union (X2 meet Y)) & (Y meet (X1 union X2)) = ((Y meet X1) union (Y meet X2))

    proof

      let Y be non empty SubSpace of X;

      assume that

       A1: X1 meets Y and

       A2: Y meets X2;

      X1 is SubSpace of (X1 union X2) by Th22;

      then

       A3: the carrier of X1 c= the carrier of (X1 union X2) by Th4;

      the carrier of X1 meets the carrier of Y by A1;

      then (the carrier of X1 /\ the carrier of Y) <> {} by XBOOLE_0:def 7;

      then (the carrier of (X1 union X2) /\ the carrier of Y) <> {} by A3, XBOOLE_1: 3, XBOOLE_1: 26;

      then the carrier of (X1 union X2) meets the carrier of Y by XBOOLE_0:def 7;

      then

       A4: (X1 union X2) meets Y;



      then the carrier of ((X1 union X2) meet Y) = (the carrier of (X1 union X2) /\ the carrier of Y) by Def4

      .= ((the carrier of X1 \/ the carrier of X2) /\ the carrier of Y) by Def2

      .= ((the carrier of X1 /\ the carrier of Y) \/ (the carrier of X2 /\ the carrier of Y)) by XBOOLE_1: 23

      .= (the carrier of (X1 meet Y) \/ (the carrier of X2 /\ the carrier of Y)) by A1, Def4

      .= (the carrier of (X1 meet Y) \/ the carrier of (X2 meet Y)) by A2, Def4

      .= the carrier of ((X1 meet Y) union (X2 meet Y)) by Def2;

      hence ((X1 union X2) meet Y) = ((X1 meet Y) union (X2 meet Y)) by Th5;



      hence (Y meet (X1 union X2)) = ((X1 meet Y) union (X2 meet Y)) by A4, Th26

      .= ((Y meet X1) union (X2 meet Y)) by A1, Th26

      .= ((Y meet X1) union (Y meet X2)) by A2, Th26;

    end;

    theorem :: TSEP_1:33

    for Y be non empty SubSpace of X holds X1 meets X2 implies ((X1 meet X2) union Y) = ((X1 union Y) meet (X2 union Y)) & (Y union (X1 meet X2)) = ((Y union X1) meet (Y union X2))

    proof

      let Y be non empty SubSpace of X;

      assume

       A1: X1 meets X2;

      Y is SubSpace of (X2 union Y) by Th22;

      then

       A2: the carrier of Y c= the carrier of (X2 union Y) by Th4;

      Y is SubSpace of (X1 union Y) by Th22;

      then the carrier of Y c= the carrier of (X1 union Y) by Th4;

      then (the carrier of (X1 union Y) /\ the carrier of (X2 union Y)) <> {} by A2, XBOOLE_1: 3, XBOOLE_1: 19;

      then the carrier of (X1 union Y) meets the carrier of (X2 union Y) by XBOOLE_0:def 7;

      then

       A3: (X1 union Y) meets (X2 union Y);



       A4: the carrier of ((X1 meet X2) union Y) = (the carrier of (X1 meet X2) \/ the carrier of Y) by Def2

      .= ((the carrier of X1 /\ the carrier of X2) \/ the carrier of Y) by A1, Def4

      .= ((the carrier of X1 \/ the carrier of Y) /\ (the carrier of X2 \/ the carrier of Y)) by XBOOLE_1: 24

      .= (the carrier of (X1 union Y) /\ (the carrier of X2 \/ the carrier of Y)) by Def2

      .= (the carrier of (X1 union Y) /\ the carrier of (X2 union Y)) by Def2

      .= the carrier of ((X1 union Y) meet (X2 union Y)) by A3, Def4;

      hence ((X1 meet X2) union Y) = ((X1 union Y) meet (X2 union Y)) by Th5;

      thus thesis by A4, Th5;

    end;

    begin

    notation

      let X be TopStruct, A1,A2 be Subset of X;

      antonym A1,A2 are_not_separated for A1,A2 are_separated ;

    end

    reserve X for TopSpace;

    reserve A1,A2 for Subset of X;

    theorem :: TSEP_1:34



     Th34: A1 is closed & A2 is closed implies (A1 misses A2 iff (A1,A2) are_separated )

    proof

      assume

       A1: A1 is closed & A2 is closed;

      thus A1 misses A2 implies (A1,A2) are_separated

      proof

        assume

         A2: A1 misses A2;

        ( Cl A1) = A1 & ( Cl A2) = A2 by A1, PRE_TOPC: 22;

        hence thesis by A2, CONNSP_1:def 1;

      end;

      thus thesis by CONNSP_1: 1;

    end;

    theorem :: TSEP_1:35



     Th35: (A1 \/ A2) is closed & (A1,A2) are_separated implies A1 is closed & A2 is closed

    proof

      assume

       A1: (A1 \/ A2) is closed;

      then ( Cl A1) c= (A1 \/ A2) by TOPS_1: 5, XBOOLE_1: 7;

      then

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

      assume

       A3: (A1,A2) are_separated ;

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

      then

       A4: ( Cl A1) c= A1 by A2, XBOOLE_1: 83;

      ( Cl A2) c= (A1 \/ A2) by A1, TOPS_1: 5, XBOOLE_1: 7;

      then

       A5: (( Cl A2) \ A1) c= A2 by XBOOLE_1: 43;

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

      then

       A6: ( Cl A2) c= A2 by A5, XBOOLE_1: 83;

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

      hence thesis by A6, A4, XBOOLE_0:def 10;

    end;

    theorem :: TSEP_1:36



     Th36: A1 misses A2 & A1 is open implies A1 misses ( Cl A2)

    proof

      assume

       A1: A1 misses A2;

      thus A1 is open implies A1 misses ( Cl A2)

      proof

        assume

         A2: A1 is open;

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

        then ( Cl A2) c= (A1 ` ) by A2, TOPS_1: 5;

        then ( Cl A2) misses ((A1 ` ) ` ) by SUBSET_1: 24;

        hence thesis;

      end;

    end;

    theorem :: TSEP_1:37



     Th37: A1 is open & A2 is open implies (A1 misses A2 iff (A1,A2) are_separated )

    proof

      assume

       A1: A1 is open & A2 is open;

      thus A1 misses A2 implies (A1,A2) are_separated

      proof

        assume A1 misses A2;

        then A1 misses ( Cl A2) & ( Cl A1) misses A2 by A1, Th36;

        hence thesis by CONNSP_1:def 1;

      end;

      thus thesis by CONNSP_1: 1;

    end;

    theorem :: TSEP_1:38



     Th38: (A1 \/ A2) is open & (A1,A2) are_separated implies A1 is open & A2 is open

    proof

      assume

       A1: (A1 \/ A2) is open;



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

      assume

       A3: (A1,A2) are_separated ;

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

      then

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

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

      then

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



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



       A7: ((A1 \/ A2) /\ (( Cl A2) ` )) = ((A1 \/ A2) \ ( Cl A2)) by SUBSET_1: 13

      .= ((A1 \ ( Cl A2)) \/ (A2 \ ( Cl A2))) by XBOOLE_1: 42

      .= ((A1 \ ( Cl A2)) \/ {} ) by A6, XBOOLE_1: 37

      .= (A1 /\ (( Cl A2) ` )) by SUBSET_1: 13

      .= A1 by A5, XBOOLE_1: 28;

      ((A1 \/ A2) /\ (( Cl A1) ` )) = ((A1 \/ A2) \ ( Cl A1)) by SUBSET_1: 13

      .= ((A1 \ ( Cl A1)) \/ (A2 \ ( Cl A1))) by XBOOLE_1: 42

      .= ( {} \/ (A2 \ ( Cl A1))) by A2, XBOOLE_1: 37

      .= (A2 /\ (( Cl A1) ` )) by SUBSET_1: 13

      .= A2 by A4, XBOOLE_1: 28;

      hence thesis by A1, A7;

    end;

    reserve A1,A2 for Subset of X;

    theorem :: TSEP_1:39



     Th39: for C be Subset of X holds (A1,A2) are_separated implies ((A1 /\ C),(A2 /\ C)) are_separated

    proof

      let C be Subset of X;



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

      assume (A1,A2) are_separated ;

      hence thesis by A1, CONNSP_1: 7;

    end;

    theorem :: TSEP_1:40



     Th40: for B be Subset of X holds (A1,B) are_separated or (A2,B) are_separated implies ((A1 /\ A2),B) are_separated

    proof

      let B be Subset of X;

      thus (A1,B) are_separated or (A2,B) are_separated implies ((A1 /\ A2),B) are_separated

      proof

         A1:

        now



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

          assume (A2,B) are_separated ;

          hence thesis by A2, CONNSP_1: 7;

        end;

         A3:

        now



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

          assume (A1,B) are_separated ;

          hence thesis by A4, CONNSP_1: 7;

        end;

        assume (A1,B) are_separated or (A2,B) are_separated ;

        hence thesis by A3, A1;

      end;

    end;

    theorem :: TSEP_1:41



     Th41: for B be Subset of X holds (A1,B) are_separated & (A2,B) are_separated iff ((A1 \/ A2),B) are_separated

    proof

      let B be Subset of X;

      ((A1 \/ A2),B) are_separated implies (A1,B) are_separated & (A2,B) are_separated

      proof



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

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

        hence thesis by A1, CONNSP_1: 7;

      end;

      hence (A1,B) are_separated & (A2,B) are_separated iff ((A1 \/ A2),B) are_separated by CONNSP_1: 8;

    end;

    theorem :: TSEP_1:42



     Th42: (A1,A2) are_separated iff ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed

    proof

      thus (A1,A2) are_separated implies ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed

      proof

        set C1 = ( Cl A1), C2 = ( Cl A2);

        assume

         A1: (A1,A2) are_separated ;

        take C1, C2;

        thus thesis by A1, CONNSP_1:def 1, PRE_TOPC: 18;

      end;

      given C1,C2 be Subset of X such that

       A2: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed;

      ( Cl A1) misses A2 & A1 misses ( Cl A2) by A2, TOPS_1: 5, XBOOLE_1: 63;

      hence thesis by CONNSP_1:def 1;

    end;

    theorem :: TSEP_1:43



     Th43: (A1,A2) are_separated iff ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & (C1 /\ C2) misses (A1 \/ A2) & C1 is closed & C2 is closed

    proof

      thus (A1,A2) are_separated implies ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & (C1 /\ C2) misses (A1 \/ A2) & C1 is closed & C2 is closed

      proof

        assume (A1,A2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A1: A1 c= C1 & A2 c= C2 and

         A2: C1 misses A2 & C2 misses A1 and

         A3: C1 is closed & C2 is closed by Th42;

        take C1, C2;

        (C1 /\ C2) misses A1 & (C1 /\ C2) misses A2 by A2, XBOOLE_1: 17, XBOOLE_1: 63;

        hence thesis by A1, A3, XBOOLE_1: 70;

      end;

      given C1,C2 be Subset of X such that

       A4: A1 c= C1 and

       A5: A2 c= C2 and

       A6: (C1 /\ C2) misses (A1 \/ A2) and

       A7: C1 is closed & C2 is closed;

      ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed

      proof

        take C1, C2;

         A8:

        now

          (A1 /\ C2) c= (C1 /\ C2) & (A1 /\ C2) c= A1 by A4, XBOOLE_1: 17, XBOOLE_1: 26;

          then

           A9: (A1 /\ C2) c= ((C1 /\ C2) /\ A1) by XBOOLE_1: 19;

          assume C2 meets A1;

          then

           A10: (A1 /\ C2) <> {} by XBOOLE_0:def 7;

          ((C1 /\ C2) /\ A1) c= ((C1 /\ C2) /\ (A1 \/ A2)) by XBOOLE_1: 7, XBOOLE_1: 26;

          then ((C1 /\ C2) /\ (A1 \/ A2)) <> {} by A10, A9, XBOOLE_1: 1, XBOOLE_1: 3;

          hence contradiction by A6, XBOOLE_0:def 7;

        end;

        now

          (C1 /\ A2) c= (C1 /\ C2) & (C1 /\ A2) c= A2 by A5, XBOOLE_1: 17, XBOOLE_1: 26;

          then

           A11: (C1 /\ A2) c= ((C1 /\ C2) /\ A2) by XBOOLE_1: 19;

          assume C1 meets A2;

          then

           A12: (C1 /\ A2) <> {} by XBOOLE_0:def 7;

          ((C1 /\ C2) /\ A2) c= ((C1 /\ C2) /\ (A1 \/ A2)) by XBOOLE_1: 7, XBOOLE_1: 26;

          then ((C1 /\ C2) /\ (A1 \/ A2)) <> {} by A12, A11, XBOOLE_1: 1, XBOOLE_1: 3;

          hence contradiction by A6, XBOOLE_0:def 7;

        end;

        hence thesis by A4, A5, A7, A8;

      end;

      hence thesis by Th42;

    end;

    theorem :: TSEP_1:44



     Th44: (A1,A2) are_separated iff ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open

    proof

      thus (A1,A2) are_separated implies ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open

      proof

        assume (A1,A2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A1: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed by Th42;

        take (C2 ` ), (C1 ` );

        thus thesis by A1, SUBSET_1: 23, SUBSET_1: 24;

      end;

      given C1,C2 be Subset of X such that

       A2: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open;

      ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed

      proof

        take (C2 ` ), (C1 ` );

        thus thesis by A2, SUBSET_1: 23, SUBSET_1: 24;

      end;

      hence thesis by Th42;

    end;

    theorem :: TSEP_1:45



     Th45: (A1,A2) are_separated iff ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & (C1 /\ C2) misses (A1 \/ A2) & C1 is open & C2 is open

    proof

      thus (A1,A2) are_separated implies ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & (C1 /\ C2) misses (A1 \/ A2) & C1 is open & C2 is open

      proof

        assume (A1,A2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A1: A1 c= C1 & A2 c= C2 and

         A2: C1 misses A2 & C2 misses A1 and

         A3: C1 is open & C2 is open by Th44;

        take C1, C2;

        (C1 /\ C2) misses A1 & (C1 /\ C2) misses A2 by A2, XBOOLE_1: 17, XBOOLE_1: 63;

        hence thesis by A1, A3, XBOOLE_1: 70;

      end;

      given C1,C2 be Subset of X such that

       A4: A1 c= C1 and

       A5: A2 c= C2 and

       A6: (C1 /\ C2) misses (A1 \/ A2) and

       A7: C1 is open & C2 is open;

      ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open

      proof

        take C1, C2;

         A8:

        now

          (A1 /\ C2) c= (C1 /\ C2) & (A1 /\ C2) c= A1 by A4, XBOOLE_1: 17, XBOOLE_1: 26;

          then

           A9: (A1 /\ C2) c= ((C1 /\ C2) /\ A1) by XBOOLE_1: 19;

          assume C2 meets A1;

          then

           A10: (A1 /\ C2) <> {} by XBOOLE_0:def 7;

          ((C1 /\ C2) /\ A1) c= ((C1 /\ C2) /\ (A1 \/ A2)) by XBOOLE_1: 7, XBOOLE_1: 26;

          then ((C1 /\ C2) /\ (A1 \/ A2)) <> {} by A10, A9, XBOOLE_1: 1, XBOOLE_1: 3;

          hence contradiction by A6, XBOOLE_0:def 7;

        end;

        now

          (C1 /\ A2) c= (C1 /\ C2) & (C1 /\ A2) c= A2 by A5, XBOOLE_1: 17, XBOOLE_1: 26;

          then

           A11: (C1 /\ A2) c= ((C1 /\ C2) /\ A2) by XBOOLE_1: 19;

          assume C1 meets A2;

          then

           A12: (C1 /\ A2) <> {} by XBOOLE_0:def 7;

          ((C1 /\ C2) /\ A2) c= ((C1 /\ C2) /\ (A1 \/ A2)) by XBOOLE_1: 7, XBOOLE_1: 26;

          then ((C1 /\ C2) /\ (A1 \/ A2)) <> {} by A12, A11, XBOOLE_1: 1, XBOOLE_1: 3;

          hence contradiction by A6, XBOOLE_0:def 7;

        end;

        hence thesis by A4, A5, A7, A8;

      end;

      hence thesis by Th44;

    end;

    definition

      let X be TopStruct, A1,A2 be Subset of X;

      :: TSEP_1:def5

      pred A1,A2 are_weakly_separated means ((A1 \ A2),(A2 \ A1)) are_separated ;

      symmetry ;

    end

    notation

      let X be TopStruct, A1,A2 be Subset of X;

      antonym A1,A2 are_not_weakly_separated for A1,A2 are_weakly_separated ;

    end

    reserve X for TopSpace,

A1,A2 for Subset of X;

    theorem :: TSEP_1:46



     Th46: A1 misses A2 & (A1,A2) are_weakly_separated iff (A1,A2) are_separated

    proof

      thus A1 misses A2 & (A1,A2) are_weakly_separated implies (A1,A2) are_separated

      proof

        assume that

         A1: A1 misses A2 and

         A2: (A1,A2) are_weakly_separated ;

        (A1 \ A2) = A1 & (A2 \ A1) = A2 by A1, XBOOLE_1: 83;

        hence thesis by A2;

      end;

      assume

       A3: (A1,A2) are_separated ;

      then A1 misses A2 by CONNSP_1: 1;

      then (A1 \ A2) = A1 & (A2 \ A1) = A2 by XBOOLE_1: 83;

      hence thesis by A3, CONNSP_1: 1;

    end;

    theorem :: TSEP_1:47



     Th47: A1 c= A2 implies (A1,A2) are_weakly_separated

    proof

       A1:

      now

        assume A1 c= A2;

        then

         A2: (A1 \ A2) = {} by XBOOLE_1: 37;

        then ( Cl (A1 \ A2)) = {} by PRE_TOPC: 22;

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

        then

         A3: ( Cl (A1 \ A2)) misses (A2 \ A1) by XBOOLE_0:def 7;

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

        then (A1 \ A2) misses ( Cl (A2 \ A1)) by XBOOLE_0:def 7;

        then ((A1 \ A2),(A2 \ A1)) are_separated by A3, CONNSP_1:def 1;

        hence thesis;

      end;

      assume A1 c= A2;

      hence thesis by A1;

    end;

    theorem :: TSEP_1:48



     Th48: for A1,A2 be Subset of X holds A1 is closed & A2 is closed implies (A1,A2) are_weakly_separated

    proof

      let A1,A2 be Subset of X;

      assume that

       A1: A1 is closed and

       A2: A2 is closed;

      ( Cl (A2 \ A1)) c= A2 by A2, TOPS_1: 5, XBOOLE_1: 36;

      then (( Cl (A2 \ A1)) \ A2) = {} by XBOOLE_1: 37;

      then

       A3: (A1 \ A2) misses ( Cl (A2 \ A1)) by Lm1;

      ( Cl (A1 \ A2)) c= A1 by A1, TOPS_1: 5, XBOOLE_1: 36;

      then (( Cl (A1 \ A2)) \ A1) = {} by XBOOLE_1: 37;

      then ( Cl (A1 \ A2)) misses (A2 \ A1) by Lm1;

      then ((A1 \ A2),(A2 \ A1)) are_separated by A3, CONNSP_1:def 1;

      hence thesis;

    end;

    theorem :: TSEP_1:49



     Th49: for A1,A2 be Subset of X holds A1 is open & A2 is open implies (A1,A2) are_weakly_separated

    proof

      let A1,A2 be Subset of X;

      assume that

       A1: A1 is open and

       A2: A2 is open;

      (A2 \ A1) misses A1 by XBOOLE_1: 79;

      then ( Cl (A2 \ A1)) misses A1 by A1, Th36;

      then

       A3: (A1 \ A2) misses ( Cl (A2 \ A1)) by XBOOLE_1: 36, XBOOLE_1: 63;

      A2 misses (A1 \ A2) by XBOOLE_1: 79;

      then A2 misses ( Cl (A1 \ A2)) by A2, Th36;

      then ( Cl (A1 \ A2)) misses (A2 \ A1) by XBOOLE_1: 36, XBOOLE_1: 63;

      then ((A1 \ A2),(A2 \ A1)) are_separated by A3, CONNSP_1:def 1;

      hence thesis;

    end;

    theorem :: TSEP_1:50



     Th50: for C be Subset of X holds (A1,A2) are_weakly_separated implies ((A1 \/ C),(A2 \/ C)) are_weakly_separated

    proof

      let C be Subset of X;

      ((A1 \/ C) \ (A2 \/ C)) = ((A1 \ (A2 \/ C)) \/ (C \ (A2 \/ C))) by XBOOLE_1: 42

      .= ((A1 \ (A2 \/ C)) \/ {} ) by XBOOLE_1: 46

      .= ((A1 \ A2) /\ (A1 \ C)) by XBOOLE_1: 53;

      then

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

      ((A2 \/ C) \ (A1 \/ C)) = ((A2 \ (A1 \/ C)) \/ (C \ (A1 \/ C))) by XBOOLE_1: 42

      .= ((A2 \ (A1 \/ C)) \/ {} ) by XBOOLE_1: 46

      .= ((A2 \ A1) /\ (A2 \ C)) by XBOOLE_1: 53;

      then

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

      assume (A1,A2) are_weakly_separated ;

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

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

      hence thesis;

    end;

    theorem :: TSEP_1:51



     Th51: for B1,B2 be Subset of X st B1 c= A2 & B2 c= A1 holds (A1,A2) are_weakly_separated implies ((A1 \/ B1),(A2 \/ B2)) are_weakly_separated

    proof

      let B1,B2 be Subset of X such that

       A1: B1 c= A2 and

       A2: B2 c= A1;

      A2 c= (A2 \/ B2) by XBOOLE_1: 7;

      then B1 c= (A2 \/ B2) by A1, XBOOLE_1: 1;

      then

       A3: (B1 \ (A2 \/ B2)) = {} by XBOOLE_1: 37;

      A1 c= (A1 \/ B1) by XBOOLE_1: 7;

      then B2 c= (A1 \/ B1) by A2, XBOOLE_1: 1;

      then

       A4: (B2 \ (A1 \/ B1)) = {} by XBOOLE_1: 37;

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

      then

       A5: ((A2 \/ B2) \ (A1 \/ B1)) c= (A2 \ A1) by A4, XBOOLE_1: 7, XBOOLE_1: 34;

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

      then

       A6: ((A1 \/ B1) \ (A2 \/ B2)) c= (A1 \ A2) by A3, XBOOLE_1: 7, XBOOLE_1: 34;

      assume (A1,A2) are_weakly_separated ;

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

      then (((A1 \/ B1) \ (A2 \/ B2)),((A2 \/ B2) \ (A1 \/ B1))) are_separated by A6, A5, CONNSP_1: 7;

      hence thesis;

    end;

    theorem :: TSEP_1:52



     Th52: for B be Subset of X holds (A1,B) are_weakly_separated & (A2,B) are_weakly_separated implies ((A1 /\ A2),B) are_weakly_separated

    proof

      let B be Subset of X;

      thus (A1,B) are_weakly_separated & (A2,B) are_weakly_separated implies ((A1 /\ A2),B) are_weakly_separated

      proof

        assume that

         A1: (A1,B) are_weakly_separated and

         A2: (A2,B) are_weakly_separated ;

        ((A2 \ B),(B \ A2)) are_separated by A2;

        then

         A3: (((A1 \ B) /\ (A2 \ B)),(B \ A2)) are_separated by Th40;

        ((A1 \ B),(B \ A1)) are_separated by A1;

        then (((A1 \ B) /\ (A2 \ B)),(B \ A1)) are_separated by Th40;

        then (((A1 \ B) /\ (A2 \ B)),((B \ A1) \/ (B \ A2))) are_separated by A3, Th41;

        then (((A1 /\ A2) \ B),((B \ A1) \/ (B \ A2))) are_separated by Lm2;

        then (((A1 /\ A2) \ B),(B \ (A1 /\ A2))) are_separated by XBOOLE_1: 54;

        hence thesis;

      end;

    end;

    theorem :: TSEP_1:53



     Th53: for B be Subset of X holds (A1,B) are_weakly_separated & (A2,B) are_weakly_separated implies ((A1 \/ A2),B) are_weakly_separated

    proof

      let B be Subset of X;

      thus (A1,B) are_weakly_separated & (A2,B) are_weakly_separated implies ((A1 \/ A2),B) are_weakly_separated

      proof

        assume that

         A1: (A1,B) are_weakly_separated and

         A2: (A2,B) are_weakly_separated ;

        ((A2 \ B),(B \ A2)) are_separated by A2;

        then

         A3: ((A2 \ B),((B \ A1) /\ (B \ A2))) are_separated by Th40;

        ((A1 \ B),(B \ A1)) are_separated by A1;

        then ((A1 \ B),((B \ A1) /\ (B \ A2))) are_separated by Th40;

        then (((A1 \ B) \/ (A2 \ B)),((B \ A1) /\ (B \ A2))) are_separated by A3, Th41;

        then (((A1 \/ A2) \ B),((B \ A1) /\ (B \ A2))) are_separated by XBOOLE_1: 42;

        then (((A1 \/ A2) \ B),(B \ (A1 \/ A2))) are_separated by XBOOLE_1: 53;

        hence thesis;

      end;

    end;

    theorem :: TSEP_1:54



     Th54: (A1,A2) are_weakly_separated iff ex C1,C2,C be Subset of X st (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is closed & C2 is closed & C is open

    proof

      set B1 = (A1 \ A2), B2 = (A2 \ A1);



       A1: ((A1 \/ A2) ` ) misses (A1 \/ A2) by XBOOLE_1: 79;

      thus (A1,A2) are_weakly_separated implies ex C1,C2,C be Subset of X st (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is closed & C2 is closed & C is open

      proof

        assume (A1,A2) are_weakly_separated ;

        then (B1,B2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A2: B1 c= C1 & B2 c= C2 and

         A3: C1 misses B2 and

         A4: C2 misses B1 and

         A5: C1 is closed & C2 is closed by Th42;

        (C1 /\ B2) = {} by A3, XBOOLE_0:def 7;

        then ((C1 /\ A2) \ (C1 /\ A1)) = {} by XBOOLE_1: 50;

        then

         A6: (C1 /\ A2) c= (C1 /\ A1) by XBOOLE_1: 37;

        take C1, C2;

        take C = ((C1 \/ C2) ` );

        (B1 \/ B2) c= (C1 \/ C2) by A2, XBOOLE_1: 13;

        then C c= ((B1 \/ B2) ` ) by SUBSET_1: 12;

        then C c= ((A1 \+\ A2) ` ) by XBOOLE_0:def 6;

        then C c= (((A1 \/ A2) \ (A1 /\ A2)) ` ) by XBOOLE_1: 101;

        then C c= (((A1 \/ A2) ` ) \/ (A1 /\ A2)) by SUBSET_1: 14;

        then (C /\ (A1 \/ A2)) c= ((((A1 \/ A2) ` ) \/ (A1 /\ A2)) /\ (A1 \/ A2)) by XBOOLE_1: 26;

        then (C /\ (A1 \/ A2)) c= ((((A1 \/ A2) ` ) /\ (A1 \/ A2)) \/ ((A1 /\ A2) /\ (A1 \/ A2))) by XBOOLE_1: 23;

        then

         A7: (C /\ (A1 \/ A2)) c= (( {} X) \/ ((A1 /\ A2) /\ (A1 \/ A2))) by A1, XBOOLE_0:def 7;

        (C2 /\ B1) = {} by A4, XBOOLE_0:def 7;

        then ((C2 /\ A1) \ (C2 /\ A2)) = {} by XBOOLE_1: 50;

        then

         A8: (C2 /\ A1) c= (C2 /\ A2) by XBOOLE_1: 37;

        (C2 /\ (A1 \/ A2)) = ((C2 /\ A1) \/ (C2 /\ A2)) by XBOOLE_1: 23;

        then

         A9: (C2 /\ (A1 \/ A2)) = (C2 /\ A2) by A8, XBOOLE_1: 12;

        (C1 /\ (A1 \/ A2)) = ((C1 /\ A1) \/ (C1 /\ A2)) by XBOOLE_1: 23;

        then

         A10: (C1 /\ (A1 \/ A2)) = (C1 /\ A1) by A6, XBOOLE_1: 12;

        ( [#] X) = (C \/ (C ` )) & ((A1 /\ A2) /\ (A1 \/ A2)) c= (A1 /\ A2) by PRE_TOPC: 2, XBOOLE_1: 17;

        hence thesis by A5, A10, A9, A7, XBOOLE_1: 1, XBOOLE_1: 17;

      end;

      given C1,C2,C be Subset of X such that

       A11: (C1 /\ (A1 \/ A2)) c= A1 and

       A12: (C2 /\ (A1 \/ A2)) c= A2 and

       A13: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

       A14: the carrier of X = ((C1 \/ C2) \/ C) and

       A15: C1 is closed & C2 is closed and C is open;

      ex C1 be Subset of X, C2 be Subset of X st B1 c= C1 & B2 c= C2 & (C1 /\ C2) misses (B1 \/ B2) & C1 is closed & C2 is closed

      proof

        ((C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2))) c= (A1 /\ A2) by A11, A12, XBOOLE_1: 27;

        then ((C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2)) c= (A1 /\ A2) by XBOOLE_1: 16;

        then (((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2)) c= (A1 /\ A2) by XBOOLE_1: 16;

        then ((C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2))) c= (A1 /\ A2) by XBOOLE_1: 16;

        then (((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2)) = {} by XBOOLE_1: 37;

        then ((C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2))) = {} by XBOOLE_1: 49;

        then

         A16: ((C1 /\ C2) /\ (B1 \/ B2)) = {} by XBOOLE_1: 55;

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

        then (C /\ (A1 \/ A2)) c= A2 by A13, XBOOLE_1: 1;

        then ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) c= A2 by A12, XBOOLE_1: 8;

        then

         A17: ((C2 \/ C) /\ (A1 \/ A2)) c= A2 by XBOOLE_1: 23;

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

        then B1 c= ((A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2))) by A17, XBOOLE_1: 35;

        then

         A18: B1 c= ((A1 \/ A2) \ (C2 \/ C)) by XBOOLE_1: 47;

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

        then (C /\ (A1 \/ A2)) c= A1 by A13, XBOOLE_1: 1;

        then ((C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2))) c= A1 by A11, XBOOLE_1: 8;

        then

         A19: ((C \/ C1) /\ (A1 \/ A2)) c= A1 by XBOOLE_1: 23;

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

        then B2 c= ((A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2))) by A19, XBOOLE_1: 35;

        then

         A20: B2 c= ((A1 \/ A2) \ (C \/ C1)) by XBOOLE_1: 47;

        take C1, C2;



         A21: (A1 \/ A2) c= ( [#] X);

        then (A1 \/ A2) c= ((C2 \/ C) \/ C1) by A14, XBOOLE_1: 4;

        then

         A22: ((A1 \/ A2) \ (C2 \/ C)) c= C1 by XBOOLE_1: 43;

        (A1 \/ A2) c= ((C \/ C1) \/ C2) by A14, A21, XBOOLE_1: 4;

        then ((A1 \/ A2) \ (C \/ C1)) c= C2 by XBOOLE_1: 43;

        hence thesis by A15, A20, A18, A22, A16, XBOOLE_0:def 7, XBOOLE_1: 1;

      end;

      then (B1,B2) are_separated by Th43;

      hence thesis;

    end;

    reserve X for non empty TopSpace,

A1,A2 for Subset of X;

    theorem :: TSEP_1:55



     Th55: (A1,A2) are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1,C2 be non empty Subset of X st C1 is closed & C2 is closed & (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & ((A1 \/ A2) c= (C1 \/ C2) or ex C be non empty Subset of X st C is open & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C))

    proof

      assume that

       A1: (A1,A2) are_weakly_separated and

       A2: not A1 c= A2 and

       A3: not A2 c= A1;

      set B1 = (A1 \ A2), B2 = (A2 \ A1);



       A4: B1 <> {} by A2, XBOOLE_1: 37;



       A5: B2 <> {} by A3, XBOOLE_1: 37;



       A6: A1 c= (A1 \/ A2) by XBOOLE_1: 7;



       A7: A2 c= (A1 \/ A2) by XBOOLE_1: 7;

      consider C1,C2,C be Subset of X such that

       A8: (C1 /\ (A1 \/ A2)) c= A1 and

       A9: (C2 /\ (A1 \/ A2)) c= A2 and

       A10: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

       A11: the carrier of X = ((C1 \/ C2) \/ C) and

       A12: C1 is closed & C2 is closed and

       A13: C is open by A1, Th54;

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

      then (C /\ (A1 \/ A2)) c= A1 by A10, XBOOLE_1: 1;

      then ((C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2))) c= A1 by A8, XBOOLE_1: 8;

      then ((C \/ C1) /\ (A1 \/ A2)) c= A1 by XBOOLE_1: 23;

      then B2 c= ((A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2))) by A7, XBOOLE_1: 35;

      then

       A14: B2 c= ((A1 \/ A2) \ (C \/ C1)) by XBOOLE_1: 47;

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

      then (C /\ (A1 \/ A2)) c= A2 by A10, XBOOLE_1: 1;

      then ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) c= A2 by A9, XBOOLE_1: 8;

      then ((C2 \/ C) /\ (A1 \/ A2)) c= A2 by XBOOLE_1: 23;

      then B1 c= ((A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2))) by A6, XBOOLE_1: 35;

      then

       A15: B1 c= ((A1 \/ A2) \ (C2 \/ C)) by XBOOLE_1: 47;



       A16: (A1 \/ A2) c= ( [#] X);

      then (A1 \/ A2) c= ((C \/ C1) \/ C2) by A11, XBOOLE_1: 4;

      then ((A1 \/ A2) \ (C \/ C1)) c= C2 by XBOOLE_1: 43;

      then

      reconsider D2 = C2 as non empty Subset of X by A14, A5, XBOOLE_1: 1, XBOOLE_1: 3;

      (A1 \/ A2) c= ((C2 \/ C) \/ C1) by A11, A16, XBOOLE_1: 4;

      then ((A1 \/ A2) \ (C2 \/ C)) c= C1 by XBOOLE_1: 43;

      then

      reconsider D1 = C1 as non empty Subset of X by A15, A4, XBOOLE_1: 1, XBOOLE_1: 3;

      take D1, D2;

      now

        assume

         A17: not (A1 \/ A2) c= (C1 \/ C2);

        thus ex C be non empty Subset of X st the carrier of X = ((C1 \/ C2) \/ C) & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & C is open

        proof

          reconsider C0 = C as non empty Subset of X by A11, A17;

          take C0;

          thus thesis by A10, A11, A13;

        end;

      end;

      hence thesis by A8, A9, A12;

    end;

    theorem :: TSEP_1:56



     Th56: (A1 \/ A2) = the carrier of X implies ((A1,A2) are_weakly_separated iff ex C1,C2,C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C1 c= A1 & C2 c= A2 & C c= (A1 /\ A2) & C1 is closed & C2 is closed & C is open)

    proof

      assume

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

      thus (A1,A2) are_weakly_separated implies ex C1,C2,C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C1 c= A1 & C2 c= A2 & C c= (A1 /\ A2) & C1 is closed & C2 is closed & C is open

      proof

        assume (A1,A2) are_weakly_separated ;

        then

        consider C1,C2,C be Subset of X such that

         A2: (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is closed & C2 is closed & C is open by Th54;

        take C1, C2, C;

        thus thesis by A1, A2, XBOOLE_1: 28;

      end;

      given C1,C2,C be Subset of X such that

       A3: (A1 \/ A2) = ((C1 \/ C2) \/ C) & C1 c= A1 & C2 c= A2 & C c= (A1 /\ A2) & C1 is closed & C2 is closed & C is open;

      ex C1,C2,C be Subset of X st (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is closed & C2 is closed & C is open

      proof

        take C1, C2, C;

        thus thesis by A1, A3, XBOOLE_1: 28;

      end;

      hence thesis by Th54;

    end;

    theorem :: TSEP_1:57



     Th57: (A1 \/ A2) = the carrier of X & (A1,A2) are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1,C2 be non empty Subset of X st C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 & ((A1 \/ A2) = (C1 \/ C2) or ex C be non empty Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is open)

    proof

      assume

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

      assume (A1,A2) are_weakly_separated & not A1 c= A2 & not A2 c= A1;

      then

      consider C1,C2 be non empty Subset of X such that

       A2: C1 is closed & C2 is closed & (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 and

       A3: (A1 \/ A2) c= (C1 \/ C2) or ex C be non empty Subset of X st C is open & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) by Th55;

      take C1, C2;

      now

        assume not (A1 \/ A2) = (C1 \/ C2);

        then

        consider C be non empty Subset of X such that

         A4: C is open & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) by A1, A3, XBOOLE_0:def 10;

        thus ex C be non empty Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is open

        proof

          take C;

          thus thesis by A1, A4, XBOOLE_1: 28;

        end;

      end;

      hence thesis by A1, A2, XBOOLE_1: 28;

    end;

    theorem :: TSEP_1:58



     Th58: (A1,A2) are_weakly_separated iff ex C1,C2,C be Subset of X st (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is open & C2 is open & C is closed

    proof

      set B1 = (A1 \ A2), B2 = (A2 \ A1);



       A1: ((A1 \/ A2) ` ) misses (A1 \/ A2) by XBOOLE_1: 79;

      thus (A1,A2) are_weakly_separated implies ex C1,C2,C be Subset of X st (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is open & C2 is open & C is closed

      proof

        assume (A1,A2) are_weakly_separated ;

        then (B1,B2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A2: B1 c= C1 & B2 c= C2 and

         A3: C1 misses B2 and

         A4: C2 misses B1 and

         A5: C1 is open & C2 is open by Th44;

        (C1 /\ B2) = {} by A3, XBOOLE_0:def 7;

        then ((C1 /\ A2) \ (C1 /\ A1)) = {} by XBOOLE_1: 50;

        then

         A6: (C1 /\ A2) c= (C1 /\ A1) by XBOOLE_1: 37;

        take C1, C2;

        take C = ((C1 \/ C2) ` );

        (B1 \/ B2) c= (C1 \/ C2) by A2, XBOOLE_1: 13;

        then C c= ((B1 \/ B2) ` ) by SUBSET_1: 12;

        then C c= ((A1 \+\ A2) ` ) by XBOOLE_0:def 6;

        then C c= (((A1 \/ A2) \ (A1 /\ A2)) ` ) by XBOOLE_1: 101;

        then C c= (((A1 \/ A2) ` ) \/ (A1 /\ A2)) by SUBSET_1: 14;

        then (C /\ (A1 \/ A2)) c= ((((A1 \/ A2) ` ) \/ (A1 /\ A2)) /\ (A1 \/ A2)) by XBOOLE_1: 26;

        then (C /\ (A1 \/ A2)) c= ((((A1 \/ A2) ` ) /\ (A1 \/ A2)) \/ ((A1 /\ A2) /\ (A1 \/ A2))) by XBOOLE_1: 23;

        then

         A7: (C /\ (A1 \/ A2)) c= (( {} X) \/ ((A1 /\ A2) /\ (A1 \/ A2))) by A1, XBOOLE_0:def 7;

        (C2 /\ B1) = {} by A4, XBOOLE_0:def 7;

        then ((C2 /\ A1) \ (C2 /\ A2)) = {} by XBOOLE_1: 50;

        then

         A8: (C2 /\ A1) c= (C2 /\ A2) by XBOOLE_1: 37;

        (C2 /\ (A1 \/ A2)) = ((C2 /\ A1) \/ (C2 /\ A2)) by XBOOLE_1: 23;

        then

         A9: (C2 /\ (A1 \/ A2)) = (C2 /\ A2) by A8, XBOOLE_1: 12;

        (C1 /\ (A1 \/ A2)) = ((C1 /\ A1) \/ (C1 /\ A2)) by XBOOLE_1: 23;

        then

         A10: (C1 /\ (A1 \/ A2)) = (C1 /\ A1) by A6, XBOOLE_1: 12;

        ( [#] X) = ((C ` ) \/ C) & ((A1 /\ A2) /\ (A1 \/ A2)) c= (A1 /\ A2) by PRE_TOPC: 2, XBOOLE_1: 17;

        hence thesis by A5, A10, A9, A7, XBOOLE_1: 1, XBOOLE_1: 17;

      end;

      given C1,C2,C be Subset of X such that

       A11: (C1 /\ (A1 \/ A2)) c= A1 and

       A12: (C2 /\ (A1 \/ A2)) c= A2 and

       A13: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

       A14: the carrier of X = ((C1 \/ C2) \/ C) and

       A15: C1 is open & C2 is open and C is closed;

      ex C1,C2 be Subset of X st B1 c= C1 & B2 c= C2 & (C1 /\ C2) misses (B1 \/ B2) & C1 is open & C2 is open

      proof

        ((C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2))) c= (A1 /\ A2) by A11, A12, XBOOLE_1: 27;

        then ((C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2)) c= (A1 /\ A2) by XBOOLE_1: 16;

        then (((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2)) c= (A1 /\ A2) by XBOOLE_1: 16;

        then ((C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2))) c= (A1 /\ A2) by XBOOLE_1: 16;

        then (((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2)) = {} by XBOOLE_1: 37;

        then ((C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2))) = {} by XBOOLE_1: 49;

        then

         A16: ((C1 /\ C2) /\ (B1 \/ B2)) = {} by XBOOLE_1: 55;

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

        then (C /\ (A1 \/ A2)) c= A2 by A13, XBOOLE_1: 1;

        then ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) c= A2 by A12, XBOOLE_1: 8;

        then

         A17: ((C2 \/ C) /\ (A1 \/ A2)) c= A2 by XBOOLE_1: 23;

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

        then B1 c= ((A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2))) by A17, XBOOLE_1: 35;

        then

         A18: B1 c= ((A1 \/ A2) \ (C2 \/ C)) by XBOOLE_1: 47;

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

        then (C /\ (A1 \/ A2)) c= A1 by A13, XBOOLE_1: 1;

        then ((C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2))) c= A1 by A11, XBOOLE_1: 8;

        then

         A19: ((C \/ C1) /\ (A1 \/ A2)) c= A1 by XBOOLE_1: 23;

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

        then B2 c= ((A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2))) by A19, XBOOLE_1: 35;

        then

         A20: B2 c= ((A1 \/ A2) \ (C \/ C1)) by XBOOLE_1: 47;

        take C1, C2;



         A21: (A1 \/ A2) c= ( [#] X);

        then (A1 \/ A2) c= ((C2 \/ C) \/ C1) by A14, XBOOLE_1: 4;

        then

         A22: ((A1 \/ A2) \ (C2 \/ C)) c= C1 by XBOOLE_1: 43;

        (A1 \/ A2) c= ((C \/ C1) \/ C2) by A14, A21, XBOOLE_1: 4;

        then ((A1 \/ A2) \ (C \/ C1)) c= C2 by XBOOLE_1: 43;

        hence thesis by A15, A20, A18, A22, A16, XBOOLE_0:def 7, XBOOLE_1: 1;

      end;

      then (B1,B2) are_separated by Th45;

      hence thesis;

    end;

    theorem :: TSEP_1:59



     Th59: (A1,A2) are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1,C2 be non empty Subset of X st C1 is open & C2 is open & (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & ((A1 \/ A2) c= (C1 \/ C2) or ex C be non empty Subset of X st C is closed & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C))

    proof

      assume that

       A1: (A1,A2) are_weakly_separated and

       A2: not A1 c= A2 and

       A3: not A2 c= A1;

      set B1 = (A1 \ A2), B2 = (A2 \ A1);



       A4: B1 <> {} by A2, XBOOLE_1: 37;



       A5: B2 <> {} by A3, XBOOLE_1: 37;



       A6: A1 c= (A1 \/ A2) by XBOOLE_1: 7;



       A7: A2 c= (A1 \/ A2) by XBOOLE_1: 7;

      consider C1,C2,C be Subset of X such that

       A8: (C1 /\ (A1 \/ A2)) c= A1 and

       A9: (C2 /\ (A1 \/ A2)) c= A2 and

       A10: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

       A11: the carrier of X = ((C1 \/ C2) \/ C) and

       A12: C1 is open & C2 is open and

       A13: C is closed by A1, Th58;

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

      then (C /\ (A1 \/ A2)) c= A1 by A10, XBOOLE_1: 1;

      then ((C /\ (A1 \/ A2)) \/ (C1 /\ (A1 \/ A2))) c= A1 by A8, XBOOLE_1: 8;

      then ((C \/ C1) /\ (A1 \/ A2)) c= A1 by XBOOLE_1: 23;

      then B2 c= ((A1 \/ A2) \ ((C \/ C1) /\ (A1 \/ A2))) by A7, XBOOLE_1: 35;

      then

       A14: B2 c= ((A1 \/ A2) \ (C \/ C1)) by XBOOLE_1: 47;

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

      then (C /\ (A1 \/ A2)) c= A2 by A10, XBOOLE_1: 1;

      then ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) c= A2 by A9, XBOOLE_1: 8;

      then ((C2 \/ C) /\ (A1 \/ A2)) c= A2 by XBOOLE_1: 23;

      then B1 c= ((A1 \/ A2) \ ((C2 \/ C) /\ (A1 \/ A2))) by A6, XBOOLE_1: 35;

      then

       A15: B1 c= ((A1 \/ A2) \ (C2 \/ C)) by XBOOLE_1: 47;



       A16: (A1 \/ A2) c= ( [#] X);

      then (A1 \/ A2) c= ((C \/ C1) \/ C2) by A11, XBOOLE_1: 4;

      then ((A1 \/ A2) \ (C \/ C1)) c= C2 by XBOOLE_1: 43;

      then

      reconsider D2 = C2 as non empty Subset of X by A14, A5, XBOOLE_1: 1, XBOOLE_1: 3;

      (A1 \/ A2) c= ((C2 \/ C) \/ C1) by A11, A16, XBOOLE_1: 4;

      then ((A1 \/ A2) \ (C2 \/ C)) c= C1 by XBOOLE_1: 43;

      then

      reconsider D1 = C1 as non empty Subset of X by A15, A4, XBOOLE_1: 1, XBOOLE_1: 3;

      take D1, D2;

      now

        assume

         A17: not (A1 \/ A2) c= (C1 \/ C2);

        thus ex C be non empty Subset of X st the carrier of X = ((C1 \/ C2) \/ C) & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & C is closed

        proof

          reconsider C0 = C as non empty Subset of X by A11, A17;

          take C0;

          thus thesis by A10, A11, A13;

        end;

      end;

      hence thesis by A8, A9, A12;

    end;

    theorem :: TSEP_1:60



     Th60: (A1 \/ A2) = the carrier of X implies ((A1,A2) are_weakly_separated iff ex C1,C2,C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C1 c= A1 & C2 c= A2 & C c= (A1 /\ A2) & C1 is open & C2 is open & C is closed)

    proof

      assume

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

      thus (A1,A2) are_weakly_separated implies ex C1,C2,C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C1 c= A1 & C2 c= A2 & C c= (A1 /\ A2) & C1 is open & C2 is open & C is closed

      proof

        assume (A1,A2) are_weakly_separated ;

        then

        consider C1,C2,C be Subset of X such that

         A2: (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is open & C2 is open & C is closed by Th58;

        take C1, C2, C;

        thus thesis by A1, A2, XBOOLE_1: 28;

      end;

      given C1,C2,C be Subset of X such that

       A3: (A1 \/ A2) = ((C1 \/ C2) \/ C) & C1 c= A1 & C2 c= A2 & C c= (A1 /\ A2) & C1 is open & C2 is open & C is closed;

      ex C1,C2,C be Subset of X st (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) & C1 is open & C2 is open & C is closed

      proof

        take C1, C2, C;

        thus thesis by A1, A3, XBOOLE_1: 28;

      end;

      hence thesis by Th58;

    end;

    theorem :: TSEP_1:61



     Th61: (A1 \/ A2) = the carrier of X & (A1,A2) are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies ex C1,C2 be non empty Subset of X st C1 is open & C2 is open & C1 c= A1 & C2 c= A2 & ((A1 \/ A2) = (C1 \/ C2) or ex C be non empty Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is closed)

    proof

      assume

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

      assume (A1,A2) are_weakly_separated & not A1 c= A2 & not A2 c= A1;

      then

      consider C1,C2 be non empty Subset of X such that

       A2: C1 is open & C2 is open & (C1 /\ (A1 \/ A2)) c= A1 & (C2 /\ (A1 \/ A2)) c= A2 and

       A3: (A1 \/ A2) c= (C1 \/ C2) or ex C be non empty Subset of X st C is closed & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) by Th59;

      take C1, C2;

      now

        assume not (A1 \/ A2) = (C1 \/ C2);

        then

        consider C be non empty Subset of X such that

         A4: C is closed & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) by A1, A3, XBOOLE_0:def 10;

        thus ex C be non empty Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is closed

        proof

          take C;

          thus thesis by A1, A4, XBOOLE_1: 28;

        end;

      end;

      hence thesis by A1, A2, XBOOLE_1: 28;

    end;

    theorem :: TSEP_1:62



     Th62: (A1,A2) are_separated iff ex B1,B2 be Subset of X st (B1,B2) are_weakly_separated & A1 c= B1 & A2 c= B2 & (B1 /\ B2) misses (A1 \/ A2)

    proof

      thus (A1,A2) are_separated implies ex B1,B2 be Subset of X st (B1,B2) are_weakly_separated & A1 c= B1 & A2 c= B2 & (B1 /\ B2) misses (A1 \/ A2)

      proof

        assume (A1,A2) are_separated ;

        then

        consider B1,B2 be Subset of X such that

         A1: A1 c= B1 & A2 c= B2 & (B1 /\ B2) misses (A1 \/ A2) & B1 is open & B2 is open by Th45;

        take B1, B2;

        thus thesis by A1, Th49;

      end;

      given B1,B2 be Subset of X such that

       A2: (B1,B2) are_weakly_separated and

       A3: A1 c= B1 and

       A4: A2 c= B2 and

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

      (B1 /\ B2) misses A1 by A5, XBOOLE_1: 7, XBOOLE_1: 63;

      then

       A6: ((B1 /\ B2) /\ A1) = {} by XBOOLE_0:def 7;

      (B1 /\ B2) misses A2 by A5, XBOOLE_1: 7, XBOOLE_1: 63;

      then

       A7: ((B1 /\ B2) /\ A2) = {} by XBOOLE_0:def 7;

      (B1 /\ A2) c= A2 & (B1 /\ A2) c= (B1 /\ B2) by A4, XBOOLE_1: 17, XBOOLE_1: 26;

      then

       A8: (B1 /\ A2) = {} by A7, XBOOLE_1: 3, XBOOLE_1: 19;

      (A2 \ B1) c= (B2 \ B1) by A4, XBOOLE_1: 33;

      then

       A9: (A2 \ (B1 /\ A2)) c= (B2 \ B1) by XBOOLE_1: 47;

      (A1 /\ B2) c= A1 & (A1 /\ B2) c= (B1 /\ B2) by A3, XBOOLE_1: 17, XBOOLE_1: 26;

      then

       A10: (A1 /\ B2) = {} by A6, XBOOLE_1: 3, XBOOLE_1: 19;

      (A1 \ B2) c= (B1 \ B2) by A3, XBOOLE_1: 33;

      then

       A11: (A1 \ (A1 /\ B2)) c= (B1 \ B2) by XBOOLE_1: 47;

      ((B1 \ B2),(B2 \ B1)) are_separated by A2;

      hence thesis by A10, A8, A11, A9, CONNSP_1: 7;

    end;

    begin

    reserve X for non empty TopSpace;

    definition

      let X be TopStruct;

      let X1,X2 be SubSpace of X;

      :: TSEP_1:def6

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

      symmetry ;

    end

    notation

      let X be TopStruct;

      let X1,X2 be SubSpace of X;

      antonym X1,X2 are_not_separated for X1,X2 are_separated ;

    end

    reserve X1,X2 for non empty SubSpace of X;

    theorem :: TSEP_1:63

    (X1,X2) are_separated implies X1 misses X2

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume (X1,X2) are_separated ;

      then (A1,A2) are_separated ;

      then A1 misses A2 by CONNSP_1: 1;

      hence thesis;

    end;

    theorem :: TSEP_1:64

    for X1,X2 be closed non empty SubSpace of X holds X1 misses X2 iff (X1,X2) are_separated

    proof

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

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;



       A1: A1 is closed & A2 is closed by Th11;

      thus X1 misses X2 implies (X1,X2) are_separated by A1, Th34;

      assume (X1,X2) are_separated ;

      then (A1,A2) are_separated ;

      then A1 misses A2 by CONNSP_1: 1;

      hence thesis;

    end;

    theorem :: TSEP_1:65

    X = (X1 union X2) & (X1,X2) are_separated implies X1 is closed SubSpace of X

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume X = (X1 union X2);

      then

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

      assume (X1,X2) are_separated ;

      then (A1,A2) are_separated ;

      then A1 is closed by A1, CONNSP_1: 4;

      hence thesis by Th11;

    end;

    theorem :: TSEP_1:66

    (X1 union X2) is closed SubSpace of X & (X1,X2) are_separated implies X1 is closed SubSpace of X

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume

       A1: (X1 union X2) is closed SubSpace of X;

      assume (X1,X2) are_separated ;

      then

       A2: (A1,A2) are_separated ;

      (A1 \/ A2) = the carrier of (X1 union X2) by Def2;

      then (A1 \/ A2) is closed by A1, Th11;

      then A1 is closed by A2, Th35;

      hence thesis by Th11;

    end;

    theorem :: TSEP_1:67

    for X1,X2 be open non empty SubSpace of X holds X1 misses X2 iff (X1,X2) are_separated

    proof

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

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;



       A1: A1 is open & A2 is open by Th16;

      thus X1 misses X2 implies (X1,X2) are_separated by A1, Th37;

      assume (X1,X2) are_separated ;

      then (A1,A2) are_separated ;

      then A1 misses A2 by CONNSP_1: 1;

      hence thesis;

    end;

    theorem :: TSEP_1:68

    X = (X1 union X2) & (X1,X2) are_separated implies X1 is open SubSpace of X

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume X = (X1 union X2);

      then

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

      assume (X1,X2) are_separated ;

      then (A1,A2) are_separated ;

      then A1 is open by A1, CONNSP_1: 4;

      hence thesis by Th16;

    end;

    theorem :: TSEP_1:69

    (X1 union X2) is open SubSpace of X & (X1,X2) are_separated implies X1 is open SubSpace of X

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume

       A1: (X1 union X2) is open SubSpace of X;

      assume (X1,X2) are_separated ;

      then

       A2: (A1,A2) are_separated ;

      (A1 \/ A2) = the carrier of (X1 union X2) by Def2;

      then (A1 \/ A2) is open by A1, Th16;

      then A1 is open by A2, Th38;

      hence thesis by Th16;

    end;

    theorem :: TSEP_1:70

    for Y,X1,X2 be non empty SubSpace of X st X1 meets Y & X2 meets Y holds (X1,X2) are_separated implies ((X1 meet Y),(X2 meet Y)) are_separated & ((Y meet X1),(Y meet X2)) are_separated

    proof

      let Y,X1,X2 be non empty SubSpace of X such that

       A1: X1 meets Y and

       A2: X2 meets Y;

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      reconsider C = the carrier of Y as Subset of X by Th1;

      assume (X1,X2) are_separated ;

      then

       A3: (A1,A2) are_separated ;

      now

        let D1,D2 be Subset of X;

        assume D1 = the carrier of (X1 meet Y) & D2 = the carrier of (X2 meet Y);

        then (A1 /\ C) = D1 & (A2 /\ C) = D2 by A1, A2, Def4;

        hence (D1,D2) are_separated by A3, Th39;

      end;

      hence ((X1 meet Y),(X2 meet Y)) are_separated ;

      then ((X1 meet Y),(Y meet X2)) are_separated by A2, Th26;

      hence ((Y meet X1),(Y meet X2)) are_separated by A1, Th26;

    end;

    theorem :: TSEP_1:71



     Th71: for Y1,Y2 be SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds (X1,X2) are_separated implies (Y1,Y2) are_separated

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      let Y1,Y2 be SubSpace of X such that

       A1: Y1 is SubSpace of X1 & Y2 is SubSpace of X2;

      assume

       A2: (X1,X2) are_separated ;

      now

        let B1,B2 be Subset of X;

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

        then

         A3: B1 c= A1 & B2 c= A2 by A1, Th4;

        (A1,A2) are_separated by A2;

        hence (B1,B2) are_separated by A3, CONNSP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:72

    for Y be non empty SubSpace of X st X1 meets X2 holds (X1,Y) are_separated implies ((X1 meet X2),Y) are_separated

    proof

      let Y be non empty SubSpace of X;

      assume X1 meets X2;

      then

       A1: (X1 meet X2) is SubSpace of X1 by Th27;

      Y is SubSpace of Y by Th2;

      hence thesis by A1, Th71;

    end;

    theorem :: TSEP_1:73

    for Y be non empty SubSpace of X holds (X1,Y) are_separated & (X2,Y) are_separated iff ((X1 union X2),Y) are_separated

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      let Y be non empty SubSpace of X;

      reconsider C = the carrier of Y as Subset of X by Th1;



       A1: Y is SubSpace of Y by Th2;

      thus (X1,Y) are_separated & (X2,Y) are_separated implies ((X1 union X2),Y) are_separated

      proof

        assume (X1,Y) are_separated & (X2,Y) are_separated ;

        then

         A2: (A1,C) are_separated & (A2,C) are_separated ;

        now

          let D,C be Subset of X;

          assume that

           A3: D = the carrier of (X1 union X2) and

           A4: C = the carrier of Y;

          (A1 \/ A2) = D by A3, Def2;

          hence (D,C) are_separated by A2, A4, Th41;

        end;

        hence thesis;

      end;

      assume

       A5: ((X1 union X2),Y) are_separated ;

      X1 is SubSpace of (X1 union X2) & X2 is SubSpace of (X1 union X2) by Th22;

      hence thesis by A5, A1, Th71;

    end;

    theorem :: TSEP_1:74

    (X1,X2) are_separated iff ex Y1,Y2 be closed non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      thus (X1,X2) are_separated implies ex Y1,Y2 be closed non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1

      proof

        assume (X1,X2) are_separated ;

        then (A1,A2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A1: A1 c= C1 and

         A2: A2 c= C2 and

         A3: C1 misses A2 & C2 misses A1 and

         A4: C1 is closed and

         A5: C2 is closed by Th42;

        C1 is non empty by A1, XBOOLE_1: 3;

        then

        consider Y1 be strict closed non empty SubSpace of X such that

         A6: C1 = the carrier of Y1 by A4, Th15;

        C2 is non empty by A2, XBOOLE_1: 3;

        then

        consider Y2 be strict closed non empty SubSpace of X such that

         A7: C2 = the carrier of Y2 by A5, Th15;

        take Y1, Y2;

        thus thesis by A1, A2, A3, A6, A7, Th4;

      end;

      given Y1,Y2 be closed non empty SubSpace of X such that

       A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1;

      now

        let A1,A2 be Subset of X such that

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

        ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed

        proof

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;

          take C1, C2;

          thus thesis by A8, A9, Th4, Th11;

        end;

        hence (A1,A2) are_separated by Th42;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:75

    (X1,X2) are_separated iff ex Y1,Y2 be closed non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2))

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      thus (X1,X2) are_separated implies ex Y1,Y2 be closed non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2))

      proof

        assume (X1,X2) are_separated ;

        then (A1,A2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A1: A1 c= C1 and

         A2: A2 c= C2 and

         A3: (C1 /\ C2) misses (A1 \/ A2) and

         A4: C1 is closed and

         A5: C2 is closed by Th43;

        C1 is non empty by A1, XBOOLE_1: 3;

        then

        consider Y1 be strict closed non empty SubSpace of X such that

         A6: C1 = the carrier of Y1 by A4, Th15;

        C2 is non empty by A2, XBOOLE_1: 3;

        then

        consider Y2 be strict closed non empty SubSpace of X such that

         A7: C2 = the carrier of Y2 by A5, Th15;

        take Y1, Y2;

        now

          assume not Y1 misses Y2;

          then

           A8: the carrier of (Y1 meet Y2) = (C1 /\ C2) by A6, A7, Def4;

          the carrier of (X1 union X2) = (A1 \/ A2) by Def2;

          hence (Y1 meet Y2) misses (X1 union X2) by A3, A8;

        end;

        hence thesis by A1, A2, A6, A7, Th4;

      end;

      given Y1,Y2 be closed non empty SubSpace of X such that

       A9: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and

       A10: Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2);

      now

        let A1,A2 be Subset of X such that

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

        ex C1 be Subset of X, C2 be Subset of X st A1 c= C1 & A2 c= C2 & (C1 /\ C2) misses (A1 \/ A2) & C1 is closed & C2 is closed

        proof

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;

          take C1, C2;

          now

            per cases ;

              suppose Y1 misses Y2;

              then C1 misses C2;

              then (C1 /\ C2) = {} by XBOOLE_0:def 7;

              hence (C1 /\ C2) misses (A1 \/ A2) by XBOOLE_1: 65;

            end;

              suppose

               A12: not Y1 misses Y2;



               A13: the carrier of (X1 union X2) = (A1 \/ A2) by A11, Def2;

              the carrier of (Y1 meet Y2) = (C1 /\ C2) by A12, Def4;

              hence (C1 /\ C2) misses (A1 \/ A2) by A10, A12, A13;

            end;

          end;

          hence thesis by A9, A11, Th4, Th11;

        end;

        hence (A1,A2) are_separated by Th43;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:76

    (X1,X2) are_separated iff ex Y1,Y2 be open non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      thus (X1,X2) are_separated implies ex Y1,Y2 be open non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1

      proof

        assume (X1,X2) are_separated ;

        then (A1,A2) are_separated ;

        then

        consider C1 be Subset of X, C2 be Subset of X such that

         A1: A1 c= C1 and

         A2: A2 c= C2 and

         A3: C1 misses A2 & C2 misses A1 and

         A4: C1 is open and

         A5: C2 is open by Th44;

        C1 is non empty by A1, XBOOLE_1: 3;

        then

        consider Y1 be strict open non empty SubSpace of X such that

         A6: C1 = the carrier of Y1 by A4, Th20;

        C2 is non empty by A2, XBOOLE_1: 3;

        then

        consider Y2 be strict open non empty SubSpace of X such that

         A7: C2 = the carrier of Y2 by A5, Th20;

        take Y1, Y2;

        thus thesis by A1, A2, A3, A6, A7, Th4;

      end;

      given Y1,Y2 be open non empty SubSpace of X such that

       A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1;

      now

        let A1,A2 be Subset of X such that

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

        ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2 is open

        proof

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;

          take C1, C2;

          thus thesis by A8, A9, Th4, Th16;

        end;

        hence (A1,A2) are_separated by Th44;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:77



     Th77: (X1,X2) are_separated iff ex Y1,Y2 be open non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2))

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      thus (X1,X2) are_separated implies ex Y1,Y2 be open non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2))

      proof

        assume (X1,X2) are_separated ;

        then (A1,A2) are_separated ;

        then

        consider C1,C2 be Subset of X such that

         A1: A1 c= C1 and

         A2: A2 c= C2 and

         A3: (C1 /\ C2) misses (A1 \/ A2) and

         A4: C1 is open and

         A5: C2 is open by Th45;

        C1 is non empty by A1, XBOOLE_1: 3;

        then

        consider Y1 be strict open non empty SubSpace of X such that

         A6: C1 = the carrier of Y1 by A4, Th20;

        C2 is non empty by A2, XBOOLE_1: 3;

        then

        consider Y2 be strict open non empty SubSpace of X such that

         A7: C2 = the carrier of Y2 by A5, Th20;

        take Y1, Y2;

        now

          assume not Y1 misses Y2;

          then

           A8: the carrier of (Y1 meet Y2) = (C1 /\ C2) by A6, A7, Def4;

          the carrier of (X1 union X2) = (A1 \/ A2) by Def2;

          hence (Y1 meet Y2) misses (X1 union X2) by A3, A8;

        end;

        hence thesis by A1, A2, A6, A7, Th4;

      end;

      given Y1,Y2 be open non empty SubSpace of X such that

       A9: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and

       A10: Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2);

      now

        let A1,A2 be Subset of X such that

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

        ex C1,C2 be Subset of X st A1 c= C1 & A2 c= C2 & (C1 /\ C2) misses (A1 \/ A2) & C1 is open & C2 is open

        proof

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;

          take C1, C2;

          now

            per cases ;

              suppose Y1 misses Y2;

              then C1 misses C2;

              then (C1 /\ C2) = {} by XBOOLE_0:def 7;

              hence (C1 /\ C2) misses (A1 \/ A2) by XBOOLE_1: 65;

            end;

              suppose

               A12: not Y1 misses Y2;



               A13: the carrier of (X1 union X2) = (A1 \/ A2) by A11, Def2;

              the carrier of (Y1 meet Y2) = (C1 /\ C2) by A12, Def4;

              hence (C1 /\ C2) misses (A1 \/ A2) by A10, A12, A13;

            end;

          end;

          hence thesis by A9, A11, Th4, Th16;

        end;

        hence (A1,A2) are_separated by Th45;

      end;

      hence thesis;

    end;

    definition

      let X be TopStruct, X1,X2 be SubSpace of X;

      :: TSEP_1:def7

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

      symmetry ;

    end

    notation

      let X be TopStruct, X1,X2 be SubSpace of X;

      antonym X1,X2 are_not_weakly_separated for X1,X2 are_weakly_separated ;

    end

    reserve X1,X2 for non empty SubSpace of X;

    theorem :: TSEP_1:78



     Th78: X1 misses X2 & (X1,X2) are_weakly_separated iff (X1,X2) are_separated

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      thus X1 misses X2 & (X1,X2) are_weakly_separated implies (X1,X2) are_separated by Th46;

      assume (X1,X2) are_separated ;

      then

       A1: (A1,A2) are_separated ;

      then A1 misses A2 by Th46;

      hence X1 misses X2;

      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, Th46;

      hence thesis;

    end;

    theorem :: TSEP_1:79



     Th79: X1 is SubSpace of X2 implies (X1,X2) are_weakly_separated by Th47, Th4;

    theorem :: TSEP_1:80



     Th80: for X1,X2 be closed SubSpace of X holds (X1,X2) are_weakly_separated

    proof

      let X1,X2 be closed SubSpace of X;

      let A1,A2 be Subset of X;

      reconsider B1 = A1, B2 = A2 as Subset of X;

      assume A1 = the carrier of X1 & A2 = the carrier of X2;

      then B1 is closed & B2 is closed by Th11;

      hence (A1,A2) are_weakly_separated by Th48;

    end;

    theorem :: TSEP_1:81



     Th81: for X1,X2 be open SubSpace of X holds (X1,X2) are_weakly_separated

    proof

      let X1,X2 be open SubSpace of X;

      let A1,A2 be Subset of X;

      reconsider B1 = A1, B2 = A2 as Subset of X;

      assume A1 = the carrier of X1 & A2 = the carrier of X2;

      then B1 is open & B2 is open by Th16;

      hence (A1,A2) are_weakly_separated by Th49;

    end;

    theorem :: TSEP_1:82

    for Y be non empty SubSpace of X holds (X1,X2) are_weakly_separated implies ((X1 union Y),(X2 union Y)) are_weakly_separated

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      let Y be non empty SubSpace of X;

      reconsider C = the carrier of Y as Subset of X by Th1;

      assume (X1,X2) are_weakly_separated ;

      then

       A1: (A1,A2) are_weakly_separated ;

      now

        let D1,D2 be Subset of X;

        assume D1 = the carrier of (X1 union Y) & D2 = the carrier of (X2 union Y);

        then (A1 \/ C) = D1 & (A2 \/ C) = D2 by Def2;

        hence (D1,D2) are_weakly_separated by A1, Th50;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:83

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

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      let Y1,Y2 be non empty SubSpace of X such that

       A1: Y1 is SubSpace of X2 & Y2 is SubSpace of X1;

      reconsider B2 = the carrier of Y2 as Subset of X by Th1;

      reconsider B1 = the carrier of Y1 as Subset of X by Th1;

      assume (X1,X2) are_weakly_separated ;

      then

       A2: (A1,A2) are_weakly_separated ;



       A3: B1 c= A2 & B2 c= A1 by A1, Th4;

       A4:

      now

        let D1,D2 be Subset of X;

        assume D1 = the carrier of (X1 union Y1) & D2 = the carrier of (X2 union Y2);

        then (A1 \/ B1) = D1 & (A2 \/ B2) = D2 by Def2;

        hence (D1,D2) are_weakly_separated by A3, A2, Th51;

      end;

      hence ((X1 union Y1),(X2 union Y2)) are_weakly_separated ;

      thus thesis by A4;

    end;

    theorem :: TSEP_1:84

    for Y,X1,X2 be non empty SubSpace of X st X1 meets X2 holds ((X1,Y) are_weakly_separated & (X2,Y) are_weakly_separated implies ((X1 meet X2),Y) are_weakly_separated ) & ((Y,X1) are_weakly_separated & (Y,X2) are_weakly_separated implies (Y,(X1 meet X2)) are_weakly_separated )

    proof

      let Y,X1,X2 be non empty SubSpace of X such that

       A1: X1 meets X2;

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      reconsider C = the carrier of Y as Subset of X by Th1;

      thus (X1,Y) are_weakly_separated & (X2,Y) are_weakly_separated implies ((X1 meet X2),Y) are_weakly_separated

      proof

        assume (X1,Y) are_weakly_separated & (X2,Y) are_weakly_separated ;

        then

         A2: (A1,C) are_weakly_separated & (A2,C) are_weakly_separated ;

        now

          let D,C be Subset of X;

          assume that

           A3: D = the carrier of (X1 meet X2) and

           A4: C = the carrier of Y;

          (A1 /\ A2) = D by A1, A3, Def4;

          hence (D,C) are_weakly_separated by A2, A4, Th52;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:85

    for Y be non empty SubSpace of X holds ((X1,Y) are_weakly_separated & (X2,Y) are_weakly_separated implies ((X1 union X2),Y) are_weakly_separated ) & ((Y,X1) are_weakly_separated & (Y,X2) are_weakly_separated implies (Y,(X1 union X2)) are_weakly_separated )

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      let Y be non empty SubSpace of X;

      reconsider C = the carrier of Y as Subset of X by Th1;

      thus (X1,Y) are_weakly_separated & (X2,Y) are_weakly_separated implies ((X1 union X2),Y) are_weakly_separated

      proof

        assume (X1,Y) are_weakly_separated & (X2,Y) are_weakly_separated ;

        then

         A1: (A1,C) are_weakly_separated & (A2,C) are_weakly_separated ;

        now

          let D,C be Subset of X;

          assume that

           A2: D = the carrier of (X1 union X2) and

           A3: C = the carrier of Y;

          (A1 \/ A2) = D by A2, Def2;

          hence (D,C) are_weakly_separated by A1, A3, Th53;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:86

    for X be non empty TopSpace, X1,X2 be non empty SubSpace of X holds X1 meets X2 implies ((X1,X2) are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be closed non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be open non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2))))

    proof

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

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume

       A1: X1 meets X2;

       A2:

      now

        assume

         A3: X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be closed non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be open non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2));

        now

          assume that

           A4: not X1 is SubSpace of X2 and

           A5: not X2 is SubSpace of X1;

          consider Y1,Y2 be closed non empty SubSpace of X such that

           A6: (Y1 meet (X1 union X2)) is SubSpace of X1 and

           A7: (Y2 meet (X1 union X2)) is SubSpace of X2 and

           A8: (X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be open non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A3, A4, A5;

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;



           A9: the carrier of (X1 union X2) = (A1 \/ A2) by Def2;



           A10: the carrier of (Y1 union Y2) = (C1 \/ C2) by Def2;

          now

            assume Y1 misses (X1 union X2);

            then

             A11: C1 misses (A1 \/ A2) by A9;

             A12:

            now

              per cases ;

                suppose (X1 union X2) is SubSpace of (Y1 union Y2);

                then (A1 \/ A2) c= (C1 \/ C2) by A9, A10, Th4;



                then

                 A13: (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ( {} \/ (C2 /\ (A1 \/ A2))) by A11, XBOOLE_0:def 7

                .= (C2 /\ (A1 \/ A2));

                then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;

                then Y2 meets (X1 union X2) by A9;

                then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A9, Def4;

                hence (A1 \/ A2) c= A2 by A7, A13, Th4;

              end;

                suppose not (X1 union X2) is SubSpace of (Y1 union Y2);

                then

                consider Y be open non empty SubSpace of X such that

                 A14: the TopStruct of X = ((Y1 union Y2) union Y) and

                 A15: (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A8;

                reconsider C = the carrier of Y as Subset of X by Th1;

                the carrier of X = ((C1 \/ C2) \/ C) by A10, A14, Def2;



                then

                 A16: (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C1 \/ (C2 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ((C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ( {} \/ ((C2 \/ C) /\ (A1 \/ A2))) by A11, XBOOLE_0:def 7

                .= ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                 A17:

                now

                  assume (C /\ (A1 \/ A2)) <> {} ;

                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y meets (X1 union X2) by A9;

                  then

                   A18: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A9, Def4;

                  the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                  then

                   A19: (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A15, A18, Th4;



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

                  then

                   A21: (C /\ (A1 \/ A2)) c= A2 by A19, XBOOLE_1: 1;

                  now

                    per cases ;

                      suppose (C2 /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A2 by A16, A19, A20, XBOOLE_1: 1;

                    end;

                      suppose (C2 /\ (A1 \/ A2)) <> {} ;

                      then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y2 meets (X1 union X2) by A9;

                      then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A9, Def4;

                      then (C2 /\ (A1 \/ A2)) c= A2 by A7, Th4;

                      hence (A1 \/ A2) c= A2 by A16, A21, XBOOLE_1: 8;

                    end;

                  end;

                  hence (A1 \/ A2) c= A2;

                end;

                now

                  assume (C2 /\ (A1 \/ A2)) <> {} ;

                  then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y2 meets (X1 union X2) by A9;

                  then

                   A22: the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A9, Def4;

                  then

                   A23: (C2 /\ (A1 \/ A2)) c= A2 by A7, Th4;

                  now

                    per cases ;

                      suppose (C /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A2 by A7, A16, A22, Th4;

                    end;

                      suppose (C /\ (A1 \/ A2)) <> {} ;

                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y meets (X1 union X2) by A9;

                      then

                       A24: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A9, Def4;

                      the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                      then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A15, A24, Th4;

                      then (A1 \/ A2) c= (A2 \/ (A1 /\ A2)) by A16, A23, XBOOLE_1: 13;

                      hence (A1 \/ A2) c= A2 by XBOOLE_1: 12, XBOOLE_1: 17;

                    end;

                  end;

                  hence (A1 \/ A2) c= A2;

                end;

                hence (A1 \/ A2) c= A2 by A16, A17;

              end;

            end;

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

            then A1 c= A2 by A12, XBOOLE_1: 1;

            hence contradiction by A4, Th4;

          end;

          then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A9, Def4;

          then

           A25: (C1 /\ (A1 \/ A2)) c= A1 by A6, Th4;

          now

            assume not Y2 meets (X1 union X2);

            then

             A26: C2 misses (A1 \/ A2) by A9;

             A27:

            now

              per cases ;

                suppose (X1 union X2) is SubSpace of (Y1 union Y2);

                then (A1 \/ A2) c= (C1 \/ C2) by A9, A10, Th4;



                then

                 A28: (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ((C1 /\ (A1 \/ A2)) \/ {} ) by A26, XBOOLE_0:def 7

                .= (C1 /\ (A1 \/ A2));

                then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;

                then Y1 meets (X1 union X2) by A9;

                then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A9, Def4;

                hence (A1 \/ A2) c= A1 by A6, A28, Th4;

              end;

                suppose not (X1 union X2) is SubSpace of (Y1 union Y2);

                then

                consider Y be open non empty SubSpace of X such that

                 A29: the TopStruct of X = ((Y1 union Y2) union Y) and

                 A30: (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A8;

                reconsider C = the carrier of Y as Subset of X by Th1;

                the carrier of X = ((C1 \/ C2) \/ C) by A10, A29, Def2;



                then

                 A31: (A1 \/ A2) = (((C2 \/ C1) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C2 \/ (C1 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ((C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ( {} \/ ((C1 \/ C) /\ (A1 \/ A2))) by A26, XBOOLE_0:def 7

                .= ((C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                 A32:

                now

                  assume (C /\ (A1 \/ A2)) <> {} ;

                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y meets (X1 union X2) by A9;

                  then

                   A33: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A9, Def4;

                  the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                  then

                   A34: (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A30, A33, Th4;



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

                  then

                   A36: (C /\ (A1 \/ A2)) c= A1 by A34, XBOOLE_1: 1;

                  now

                    per cases ;

                      suppose (C1 /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A1 by A31, A34, A35, XBOOLE_1: 1;

                    end;

                      suppose (C1 /\ (A1 \/ A2)) <> {} ;

                      then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y1 meets (X1 union X2) by A9;

                      then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A9, Def4;

                      then (C1 /\ (A1 \/ A2)) c= A1 by A6, Th4;

                      hence (A1 \/ A2) c= A1 by A31, A36, XBOOLE_1: 8;

                    end;

                  end;

                  hence (A1 \/ A2) c= A1;

                end;

                now

                  assume (C1 /\ (A1 \/ A2)) <> {} ;

                  then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y1 meets (X1 union X2) by A9;

                  then

                   A37: the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A9, Def4;

                  then

                   A38: (C1 /\ (A1 \/ A2)) c= A1 by A6, Th4;

                  now

                    per cases ;

                      suppose (C /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A1 by A6, A31, A37, Th4;

                    end;

                      suppose (C /\ (A1 \/ A2)) <> {} ;

                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y meets (X1 union X2) by A9;

                      then

                       A39: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A9, Def4;

                      the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                      then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A30, A39, Th4;

                      then (A1 \/ A2) c= (A1 \/ (A1 /\ A2)) by A31, A38, XBOOLE_1: 13;

                      hence (A1 \/ A2) c= A1 by XBOOLE_1: 12, XBOOLE_1: 17;

                    end;

                  end;

                  hence (A1 \/ A2) c= A1;

                end;

                hence (A1 \/ A2) c= A1 by A31, A32;

              end;

            end;

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

            then A2 c= A1 by A27, XBOOLE_1: 1;

            hence contradiction by A5, Th4;

          end;

          then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A9, Def4;

          then

           A40: (C2 /\ (A1 \/ A2)) c= A2 by A7, Th4;



           A41: C1 is closed & C2 is closed by Th11;

          now

            per cases ;

              suppose

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

              thus ex C be Subset of X st the carrier of X = ((C1 \/ C2) \/ C) & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & C is open

              proof

                take C = ((C1 \/ C2) ` );

                C misses (A1 \/ A2) by A42, SUBSET_1: 24;

                then (C /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

                hence thesis by A41, PRE_TOPC: 2, XBOOLE_1: 2;

              end;

            end;

              suppose

               A43: not (A1 \/ A2) c= (C1 \/ C2);

              thus ex C be Subset of X st the carrier of X = ((C1 \/ C2) \/ C) & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & C is open

              proof

                consider Y be open non empty SubSpace of X such that

                 A44: the TopStruct of X = ((Y1 union Y2) union Y) and

                 A45: (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A8, A9, A10, A43, Th4;

                reconsider C = the carrier of Y as Subset of X by Th1;



                 A46: the carrier of X = (the carrier of (Y1 union Y2) \/ C) by A44, Def2

                .= ((C1 \/ C2) \/ C) by Def2;

                now

                  assume not Y meets (X1 union X2);

                  then

                   A47: C misses (A1 \/ A2) by A9;

                  the carrier of X = ((C1 \/ C2) \/ C) by A10, A44, Def2;



                  then (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

                  .= (((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23

                  .= (((C1 \/ C2) /\ (A1 \/ A2)) \/ {} ) by A47, XBOOLE_0:def 7

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

                  hence contradiction by A43, XBOOLE_1: 17;

                end;

                then

                 A48: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A9, Def4;



                 A49: C is open by Th16;

                the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A45, A48, Th4;

                hence thesis by A49, A46;

              end;

            end;

          end;

          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 A41, A25, A40, Th54;

          hence (X1,X2) are_weakly_separated ;

        end;

        hence (X1,X2) are_weakly_separated by Th79;

      end;



       A50: X is SubSpace of X by Th2;

      now

        assume (X1,X2) are_weakly_separated ;

        then

         A51: (A1,A2) are_weakly_separated ;

        now

          assume that

           A52: not X1 is SubSpace of X2 and

           A53: not X2 is SubSpace of X1;



           A54: not A2 c= A1 by A53, Th4;



           A55: not A1 c= A2 by A52, Th4;

          then

          consider C1,C2 be non empty Subset of X such that

           A56: C1 is closed and

           A57: C2 is closed and

           A58: (C1 /\ (A1 \/ A2)) c= A1 and

           A59: (C2 /\ (A1 \/ A2)) c= A2 and

           A60: (A1 \/ A2) c= (C1 \/ C2) or ex C be non empty Subset of X st C is open & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) by A51, A54, Th55;

           A61:

          now

            assume C2 misses (A1 \/ A2);

            then

             A62: (C2 /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

            now

              per cases ;

                suppose

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



                 A64: A2 c= (A1 \/ A2) by XBOOLE_1: 7;

                (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by A63, XBOOLE_1: 28

                .= ((C1 /\ (A1 \/ A2)) \/ {} ) by A62, XBOOLE_1: 23

                .= (C1 /\ (A1 \/ A2));

                hence contradiction by A54, A58, A64, XBOOLE_1: 1;

              end;

                suppose not (A1 \/ A2) c= (C1 \/ C2);

                then

                consider C be non empty Subset of X such that C is open and

                 A65: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

                 A66: the carrier of X = ((C1 \/ C2) \/ C) by A60;

                (A1 \/ A2) = (((C2 \/ C1) \/ C) /\ (A1 \/ A2)) by A66, XBOOLE_1: 28

                .= ((C2 \/ (C1 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ( {} \/ ((C1 \/ C) /\ (A1 \/ A2))) by A62, XBOOLE_1: 23

                .= ((C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                then (A1 \/ A2) c= (A1 \/ (A1 /\ A2)) by A58, A65, XBOOLE_1: 13;

                then

                 A67: (A1 \/ A2) c= A1 by XBOOLE_1: 12, XBOOLE_1: 17;

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

                hence contradiction by A54, A67, XBOOLE_1: 1;

              end;

            end;

            hence contradiction;

          end;

           A68:

          now

            assume C1 misses (A1 \/ A2);

            then

             A69: (C1 /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

            now

              per cases ;

                suppose

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



                 A71: A1 c= (A1 \/ A2) by XBOOLE_1: 7;

                (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by A70, XBOOLE_1: 28

                .= ( {} \/ (C2 /\ (A1 \/ A2))) by A69, XBOOLE_1: 23

                .= (C2 /\ (A1 \/ A2));

                hence contradiction by A55, A59, A71, XBOOLE_1: 1;

              end;

                suppose not (A1 \/ A2) c= (C1 \/ C2);

                then

                consider C be non empty Subset of X such that C is open and

                 A72: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

                 A73: the carrier of X = ((C1 \/ C2) \/ C) by A60;

                (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by A73, XBOOLE_1: 28

                .= ((C1 \/ (C2 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ( {} \/ ((C2 \/ C) /\ (A1 \/ A2))) by A69, XBOOLE_1: 23

                .= ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                then (A1 \/ A2) c= (A2 \/ (A1 /\ A2)) by A59, A72, XBOOLE_1: 13;

                then

                 A74: (A1 \/ A2) c= A2 by XBOOLE_1: 12, XBOOLE_1: 17;

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

                hence contradiction by A55, A74, XBOOLE_1: 1;

              end;

            end;

            hence contradiction;

          end;

          thus ex Y1,Y2 be closed non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be open non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2))

          proof

            consider Y2 be strict closed non empty SubSpace of X such that

             A75: C2 = the carrier of Y2 by A57, Th15;



             A76: the carrier of (X1 union X2) = (A1 \/ A2) by Def2;

            then Y2 meets (X1 union X2) by A61, A75;

            then

             A77: the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A75, A76, Def4;

            consider Y1 be strict closed non empty SubSpace of X such that

             A78: C1 = the carrier of Y1 by A56, Th15;



             A79: the carrier of (Y1 union Y2) = (C1 \/ C2) by A78, A75, Def2;

             A80:

            now

              assume

               A81: not (X1 union X2) is SubSpace of (Y1 union Y2);

              then

              consider C be non empty Subset of X such that

               A82: C is open and

               A83: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

               A84: the carrier of X = ((C1 \/ C2) \/ C) by A60, A76, A79, Th4;



               A85: not (A1 \/ A2) c= (C1 \/ C2) by A76, A79, A81, Th4;

              thus ex Y be open non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2)

              proof

                consider Y be strict open non empty SubSpace of X such that

                 A86: C = the carrier of Y by A82, Th20;

                now

                  assume C misses (A1 \/ A2);

                  then

                   A87: (C /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

                  (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by A84, XBOOLE_1: 28

                  .= (((C1 \/ C2) /\ (A1 \/ A2)) \/ {} ) by A87, XBOOLE_1: 23

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

                  hence contradiction by A85, XBOOLE_1: 17;

                end;

                then Y meets (X1 union X2) by A76, A86;

                then

                 A88: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A76, A86, Def4;

                take Y;



                 A89: the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                the carrier of X = (the carrier of (Y1 union Y2) \/ C) by A78, A75, A84, Def2

                .= the carrier of ((Y1 union Y2) union Y) by A86, Def2;

                hence thesis by A50, A83, A88, A89, Th4, Th5;

              end;

            end;

            take Y1, Y2;

            Y1 meets (X1 union X2) by A68, A78, A76;

            then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A78, A76, Def4;

            hence thesis by A58, A59, A77, A80, Th4;

          end;

        end;

        hence X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be closed non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be open non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2));

      end;

      hence thesis by A2;

    end;

    theorem :: TSEP_1:87

    X = (X1 union X2) & X1 meets X2 implies ((X1,X2) are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be closed non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be open non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2))))

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume

       A1: X = (X1 union X2);

      then

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

      assume

       A3: X1 meets X2;

       A4:

      now

        assume

         A5: X1 is SubSpace of X2 or X2 is SubSpace of X1 or ( not X1 is SubSpace of X2 & not X2 is SubSpace of X1 implies ex Y1,Y2 be closed non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be open non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2)));

        now

          assume ( not X1 is SubSpace of X2) & not X2 is SubSpace of X1;

          then

          consider Y1,Y2 be closed non empty SubSpace of X such that

           A6: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and

           A7: X = (Y1 union Y2) or ex Y be open non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2) by A5;

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;

           A8:

          now

            per cases ;

              suppose

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

              thus ex C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is open

              proof

                take ( {} X);

                thus thesis by A9, XBOOLE_1: 2;

              end;

            end;

              suppose

               A10: (A1 \/ A2) <> (C1 \/ C2);

              thus ex C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is open

              proof

                consider Y be open non empty SubSpace of X such that

                 A11: X = ((Y1 union Y2) union Y) and

                 A12: Y is SubSpace of (X1 meet X2) by A2, A7, A10, Def2;

                reconsider C = the carrier of Y as Subset of X by Th1;

                (A1 /\ A2) = the carrier of (X1 meet X2) by A3, Def4;

                then

                 A13: C c= (A1 /\ A2) by A12, Th4;



                 A14: C is open by Th16;

                (A1 \/ A2) = (the carrier of (Y1 union Y2) \/ C) by A2, A11, Def2

                .= ((C1 \/ C2) \/ C) by Def2;

                hence thesis by A14, A13;

              end;

            end;

          end;



           A15: C1 is closed & C2 is closed by Th11;

          C1 c= A1 & C2 c= A2 by A6, Th4;

          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 A2, A15, A8, Th56;

          hence (X1,X2) are_weakly_separated ;

        end;

        hence (X1,X2) are_weakly_separated by Th79;

      end;

      now

        assume (X1,X2) are_weakly_separated ;

        then

         A16: (A1,A2) are_weakly_separated ;

        now

          assume ( not X1 is SubSpace of X2) & not X2 is SubSpace of X1;

          then ( not A1 c= A2) & not A2 c= A1 by Th4;

          then

          consider C1,C2 be non empty Subset of X such that

           A17: C1 is closed and

           A18: C2 is closed and

           A19: C1 c= A1 & C2 c= A2 and

           A20: (A1 \/ A2) = (C1 \/ C2) or ex C be non empty Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is open by A2, A16, Th57;

          thus ex Y1,Y2 be closed non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be open non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2))

          proof

            consider Y2 be strict closed non empty SubSpace of X such that

             A21: C2 = the carrier of Y2 by A18, Th15;

            consider Y1 be strict closed non empty SubSpace of X such that

             A22: C1 = the carrier of Y1 by A17, Th15;

            take Y1, Y2;

            now

              assume X <> (Y1 union Y2);

              then

              consider C be non empty Subset of X such that

               A23: (A1 \/ A2) = ((C1 \/ C2) \/ C) and

               A24: C c= (A1 /\ A2) and

               A25: C is open by A1, A2, A20, A22, A21, Def2;

              thus ex Y be open non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2)

              proof



                 A26: C c= the carrier of (X1 meet X2) by A3, A24, Def4;

                consider Y be strict open non empty SubSpace of X such that

                 A27: C = the carrier of Y by A25, Th20;

                take Y;

                the carrier of X = (the carrier of (Y1 union Y2) \/ C) by A2, A22, A21, A23, Def2

                .= the carrier of ((Y1 union Y2) union Y) by A27, Def2;

                hence thesis by A1, A27, A26, Th4, Th5;

              end;

            end;

            hence thesis by A19, A22, A21, Th4;

          end;

        end;

        hence X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be closed non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be open non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2));

      end;

      hence thesis by A4;

    end;

    theorem :: TSEP_1:88

    X = (X1 union X2) & X1 misses X2 implies ((X1,X2) are_weakly_separated iff X1 is closed SubSpace of X & X2 is closed SubSpace of X)

    proof

      assume

       A1: X = (X1 union X2);

      assume

       A2: X1 misses X2;

      thus (X1,X2) are_weakly_separated implies X1 is closed SubSpace of X & X2 is closed SubSpace of X

      proof

        reconsider A2 = the carrier of X2 as Subset of X by Th1;

        reconsider A1 = the carrier of X1 as Subset of X by Th1;

        assume (X1,X2) are_weakly_separated ;

        then (X1,X2) are_separated by A2, Th78;

        then

         A3: (A1,A2) are_separated ;

        (A1 \/ A2) = ( [#] X) by A1, Def2;

        then A1 is closed & A2 is closed by A3, CONNSP_1: 4;

        hence thesis by Th11;

      end;

      thus thesis by Th80;

    end;

    theorem :: TSEP_1:89

    for X be non empty TopSpace, X1,X2 be non empty SubSpace of X holds X1 meets X2 implies ((X1,X2) are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be open non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be closed non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2))))

    proof

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

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume

       A1: X1 meets X2;



       A2: ( [#] X) = the carrier of X;

       A3:

      now

        assume

         A4: X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be open non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be closed non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2));

        now

          assume that

           A5: not X1 is SubSpace of X2 and

           A6: not X2 is SubSpace of X1;

          consider Y1,Y2 be open non empty SubSpace of X such that

           A7: (Y1 meet (X1 union X2)) is SubSpace of X1 and

           A8: (Y2 meet (X1 union X2)) is SubSpace of X2 and

           A9: (X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be closed non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A4, A5, A6;

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;



           A10: the carrier of (X1 union X2) = (A1 \/ A2) by Def2;



           A11: the carrier of (Y1 union Y2) = (C1 \/ C2) by Def2;

          now

            assume Y1 misses (X1 union X2);

            then

             A12: C1 misses (A1 \/ A2) by A10;

             A13:

            now

              per cases ;

                suppose (X1 union X2) is SubSpace of (Y1 union Y2);

                then (A1 \/ A2) c= (C1 \/ C2) by A10, A11, Th4;



                then

                 A14: (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ( {} \/ (C2 /\ (A1 \/ A2))) by A12, XBOOLE_0:def 7

                .= (C2 /\ (A1 \/ A2));

                then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;

                then Y2 meets (X1 union X2) by A10;

                then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A10, Def4;

                hence (A1 \/ A2) c= A2 by A8, A14, Th4;

              end;

                suppose not (X1 union X2) is SubSpace of (Y1 union Y2);

                then

                consider Y be closed non empty SubSpace of X such that

                 A15: the TopStruct of X = ((Y1 union Y2) union Y) and

                 A16: (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A9;

                reconsider C = the carrier of Y as Subset of X by Th1;

                the carrier of X = ((C1 \/ C2) \/ C) by A11, A15, Def2;



                then

                 A17: (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C1 \/ (C2 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ((C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ( {} \/ ((C2 \/ C) /\ (A1 \/ A2))) by A12, XBOOLE_0:def 7

                .= ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                 A18:

                now

                  assume (C /\ (A1 \/ A2)) <> {} ;

                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y meets (X1 union X2) by A10;

                  then

                   A19: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A10, Def4;

                  the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                  then

                   A20: (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A16, A19, Th4;



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

                  then

                   A22: (C /\ (A1 \/ A2)) c= A2 by A20, XBOOLE_1: 1;

                  now

                    per cases ;

                      suppose (C2 /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A2 by A17, A20, A21, XBOOLE_1: 1;

                    end;

                      suppose (C2 /\ (A1 \/ A2)) <> {} ;

                      then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y2 meets (X1 union X2) by A10;

                      then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A10, Def4;

                      then (C2 /\ (A1 \/ A2)) c= A2 by A8, Th4;

                      hence (A1 \/ A2) c= A2 by A17, A22, XBOOLE_1: 8;

                    end;

                  end;

                  hence (A1 \/ A2) c= A2;

                end;

                now

                  assume (C2 /\ (A1 \/ A2)) <> {} ;

                  then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y2 meets (X1 union X2) by A10;

                  then

                   A23: the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A10, Def4;

                  then

                   A24: (C2 /\ (A1 \/ A2)) c= A2 by A8, Th4;

                  now

                    per cases ;

                      suppose (C /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A2 by A8, A17, A23, Th4;

                    end;

                      suppose (C /\ (A1 \/ A2)) <> {} ;

                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y meets (X1 union X2) by A10;

                      then

                       A25: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A10, Def4;

                      the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                      then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A16, A25, Th4;

                      then (A1 \/ A2) c= (A2 \/ (A1 /\ A2)) by A17, A24, XBOOLE_1: 13;

                      hence (A1 \/ A2) c= A2 by XBOOLE_1: 12, XBOOLE_1: 17;

                    end;

                  end;

                  hence (A1 \/ A2) c= A2;

                end;

                hence (A1 \/ A2) c= A2 by A17, A18;

              end;

            end;

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

            then A1 c= A2 by A13, XBOOLE_1: 1;

            hence contradiction by A5, Th4;

          end;

          then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A10, Def4;

          then

           A26: (C1 /\ (A1 \/ A2)) c= A1 by A7, Th4;

          now

            assume not Y2 meets (X1 union X2);

            then

             A27: C2 misses (A1 \/ A2) by A10;

             A28:

            now

              per cases ;

                suppose (X1 union X2) is SubSpace of (Y1 union Y2);

                then (A1 \/ A2) c= (C1 \/ C2) by A10, A11, Th4;



                then

                 A29: (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ((C1 /\ (A1 \/ A2)) \/ {} ) by A27, XBOOLE_0:def 7

                .= (C1 /\ (A1 \/ A2));

                then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;

                then Y1 meets (X1 union X2) by A10;

                then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A10, Def4;

                hence (A1 \/ A2) c= A1 by A7, A29, Th4;

              end;

                suppose not (X1 union X2) is SubSpace of (Y1 union Y2);

                then

                consider Y be closed non empty SubSpace of X such that

                 A30: the TopStruct of X = ((Y1 union Y2) union Y) and

                 A31: (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A9;

                reconsider C = the carrier of Y as Subset of X by Th1;

                the carrier of X = ((C1 \/ C2) \/ C) by A11, A30, Def2;



                then

                 A32: (A1 \/ A2) = (((C2 \/ C1) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

                .= ((C2 \/ (C1 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ((C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2))) by XBOOLE_1: 23

                .= ( {} \/ ((C1 \/ C) /\ (A1 \/ A2))) by A27, XBOOLE_0:def 7

                .= ((C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                 A33:

                now

                  assume (C /\ (A1 \/ A2)) <> {} ;

                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y meets (X1 union X2) by A10;

                  then

                   A34: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A10, Def4;

                  the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                  then

                   A35: (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A31, A34, Th4;



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

                  then

                   A37: (C /\ (A1 \/ A2)) c= A1 by A35, XBOOLE_1: 1;

                  now

                    per cases ;

                      suppose (C1 /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A1 by A32, A35, A36, XBOOLE_1: 1;

                    end;

                      suppose (C1 /\ (A1 \/ A2)) <> {} ;

                      then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y1 meets (X1 union X2) by A10;

                      then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A10, Def4;

                      then (C1 /\ (A1 \/ A2)) c= A1 by A7, Th4;

                      hence (A1 \/ A2) c= A1 by A32, A37, XBOOLE_1: 8;

                    end;

                  end;

                  hence (A1 \/ A2) c= A1;

                end;

                now

                  assume (C1 /\ (A1 \/ A2)) <> {} ;

                  then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;

                  then Y1 meets (X1 union X2) by A10;

                  then

                   A38: the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A10, Def4;

                  then

                   A39: (C1 /\ (A1 \/ A2)) c= A1 by A7, Th4;

                  now

                    per cases ;

                      suppose (C /\ (A1 \/ A2)) = {} ;

                      hence (A1 \/ A2) c= A1 by A7, A32, A38, Th4;

                    end;

                      suppose (C /\ (A1 \/ A2)) <> {} ;

                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;

                      then Y meets (X1 union X2) by A10;

                      then

                       A40: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A10, Def4;

                      the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                      then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A31, A40, Th4;

                      then (A1 \/ A2) c= (A1 \/ (A1 /\ A2)) by A32, A39, XBOOLE_1: 13;

                      hence (A1 \/ A2) c= A1 by XBOOLE_1: 12, XBOOLE_1: 17;

                    end;

                  end;

                  hence (A1 \/ A2) c= A1;

                end;

                hence (A1 \/ A2) c= A1 by A32, A33;

              end;

            end;

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

            then A2 c= A1 by A28, XBOOLE_1: 1;

            hence contradiction by A6, Th4;

          end;

          then the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A10, Def4;

          then

           A41: (C2 /\ (A1 \/ A2)) c= A2 by A8, Th4;



           A42: C1 is open & C2 is open by Th16;

          now

            per cases ;

              suppose

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

              thus ex C be Subset of X st the carrier of X = ((C1 \/ C2) \/ C) & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & C is closed

              proof

                take C = ((C1 \/ C2) ` );

                C misses (A1 \/ A2) by A43, SUBSET_1: 24;

                then (C /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

                hence thesis by A2, A42, PRE_TOPC: 2, XBOOLE_1: 2;

              end;

            end;

              suppose

               A44: not (A1 \/ A2) c= (C1 \/ C2);

              thus ex C be Subset of X st the carrier of X = ((C1 \/ C2) \/ C) & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & C is closed

              proof

                consider Y be closed non empty SubSpace of X such that

                 A45: the TopStruct of X = ((Y1 union Y2) union Y) and

                 A46: (Y meet (X1 union X2)) is SubSpace of (X1 meet X2) by A9, A10, A11, A44, Th4;

                reconsider C = the carrier of Y as Subset of X by Th1;



                 A47: the carrier of X = (the carrier of (Y1 union Y2) \/ C) by A45, Def2

                .= ((C1 \/ C2) \/ C) by Def2;

                now

                  assume not Y meets (X1 union X2);

                  then

                   A48: C misses (A1 \/ A2) by A10;

                  the carrier of X = ((C1 \/ C2) \/ C) by A11, A45, Def2;



                  then (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by XBOOLE_1: 28

                  .= (((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23

                  .= (((C1 \/ C2) /\ (A1 \/ A2)) \/ {} ) by A48, XBOOLE_0:def 7

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

                  hence contradiction by A44, XBOOLE_1: 17;

                end;

                then

                 A49: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A10, Def4;



                 A50: C is closed by Th11;

                the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                then (C /\ (A1 \/ A2)) c= (A1 /\ A2) by A46, A49, Th4;

                hence thesis by A50, A47;

              end;

            end;

          end;

          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 A42, A26, A41, Th58;

          hence (X1,X2) are_weakly_separated ;

        end;

        hence (X1,X2) are_weakly_separated by Th79;

      end;



       A51: X is SubSpace of X by Th2;

      now

        assume (X1,X2) are_weakly_separated ;

        then

         A52: (A1,A2) are_weakly_separated ;

        now

          assume that

           A53: not X1 is SubSpace of X2 and

           A54: not X2 is SubSpace of X1;



           A55: not A2 c= A1 by A54, Th4;



           A56: not A1 c= A2 by A53, Th4;

          then

          consider C1,C2 be non empty Subset of X such that

           A57: C1 is open and

           A58: C2 is open and

           A59: (C1 /\ (A1 \/ A2)) c= A1 and

           A60: (C2 /\ (A1 \/ A2)) c= A2 and

           A61: (A1 \/ A2) c= (C1 \/ C2) or ex C be non empty Subset of X st C is closed & (C /\ (A1 \/ A2)) c= (A1 /\ A2) & the carrier of X = ((C1 \/ C2) \/ C) by A52, A55, Th59;

           A62:

          now

            assume C2 misses (A1 \/ A2);

            then

             A63: (C2 /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

            now

              per cases ;

                suppose

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



                 A65: A2 c= (A1 \/ A2) by XBOOLE_1: 7;

                (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by A64, XBOOLE_1: 28

                .= ((C1 /\ (A1 \/ A2)) \/ {} ) by A63, XBOOLE_1: 23

                .= (C1 /\ (A1 \/ A2));

                hence contradiction by A55, A59, A65, XBOOLE_1: 1;

              end;

                suppose not (A1 \/ A2) c= (C1 \/ C2);

                then

                consider C be non empty Subset of X such that C is closed and

                 A66: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

                 A67: the carrier of X = ((C1 \/ C2) \/ C) by A61;

                (A1 \/ A2) = (((C2 \/ C1) \/ C) /\ (A1 \/ A2)) by A67, XBOOLE_1: 28

                .= ((C2 \/ (C1 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ( {} \/ ((C1 \/ C) /\ (A1 \/ A2))) by A63, XBOOLE_1: 23

                .= ((C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                then (A1 \/ A2) c= (A1 \/ (A1 /\ A2)) by A59, A66, XBOOLE_1: 13;

                then

                 A68: (A1 \/ A2) c= A1 by XBOOLE_1: 12, XBOOLE_1: 17;

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

                hence contradiction by A55, A68, XBOOLE_1: 1;

              end;

            end;

            hence contradiction;

          end;

           A69:

          now

            assume C1 misses (A1 \/ A2);

            then

             A70: (C1 /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

            now

              per cases ;

                suppose

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



                 A72: A1 c= (A1 \/ A2) by XBOOLE_1: 7;

                (A1 \/ A2) = ((C1 \/ C2) /\ (A1 \/ A2)) by A71, XBOOLE_1: 28

                .= ( {} \/ (C2 /\ (A1 \/ A2))) by A70, XBOOLE_1: 23

                .= (C2 /\ (A1 \/ A2));

                hence contradiction by A56, A60, A72, XBOOLE_1: 1;

              end;

                suppose not (A1 \/ A2) c= (C1 \/ C2);

                then

                consider C be non empty Subset of X such that C is closed and

                 A73: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

                 A74: the carrier of X = ((C1 \/ C2) \/ C) by A61;

                (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by A74, XBOOLE_1: 28

                .= ((C1 \/ (C2 \/ C)) /\ (A1 \/ A2)) by XBOOLE_1: 4

                .= ( {} \/ ((C2 \/ C) /\ (A1 \/ A2))) by A70, XBOOLE_1: 23

                .= ((C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2))) by XBOOLE_1: 23;

                then (A1 \/ A2) c= (A2 \/ (A1 /\ A2)) by A60, A73, XBOOLE_1: 13;

                then

                 A75: (A1 \/ A2) c= A2 by XBOOLE_1: 12, XBOOLE_1: 17;

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

                hence contradiction by A56, A75, XBOOLE_1: 1;

              end;

            end;

            hence contradiction;

          end;

          thus ex Y1,Y2 be open non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be closed non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2))

          proof

            consider Y2 be strict open non empty SubSpace of X such that

             A76: C2 = the carrier of Y2 by A58, Th20;



             A77: the carrier of (X1 union X2) = (A1 \/ A2) by Def2;

            then Y2 meets (X1 union X2) by A62, A76;

            then

             A78: the carrier of (Y2 meet (X1 union X2)) = (C2 /\ (A1 \/ A2)) by A76, A77, Def4;

            consider Y1 be strict open non empty SubSpace of X such that

             A79: C1 = the carrier of Y1 by A57, Th20;



             A80: the carrier of (Y1 union Y2) = (C1 \/ C2) by A79, A76, Def2;

             A81:

            now

              assume

               A82: not (X1 union X2) is SubSpace of (Y1 union Y2);

              then

              consider C be non empty Subset of X such that

               A83: C is closed and

               A84: (C /\ (A1 \/ A2)) c= (A1 /\ A2) and

               A85: the carrier of X = ((C1 \/ C2) \/ C) by A61, A77, A80, Th4;



               A86: not (A1 \/ A2) c= (C1 \/ C2) by A77, A80, A82, Th4;

              thus ex Y be closed non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2)

              proof

                consider Y be strict closed non empty SubSpace of X such that

                 A87: C = the carrier of Y by A83, Th15;

                now

                  assume C misses (A1 \/ A2);

                  then

                   A88: (C /\ (A1 \/ A2)) = {} by XBOOLE_0:def 7;

                  (A1 \/ A2) = (((C1 \/ C2) \/ C) /\ (A1 \/ A2)) by A85, XBOOLE_1: 28

                  .= (((C1 \/ C2) /\ (A1 \/ A2)) \/ {} ) by A88, XBOOLE_1: 23

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

                  hence contradiction by A86, XBOOLE_1: 17;

                end;

                then Y meets (X1 union X2) by A77, A87;

                then

                 A89: the carrier of (Y meet (X1 union X2)) = (C /\ (A1 \/ A2)) by A77, A87, Def4;

                take Y;



                 A90: the carrier of (X1 meet X2) = (A1 /\ A2) by A1, Def4;

                the carrier of X = (the carrier of (Y1 union Y2) \/ C) by A79, A76, A85, Def2

                .= the carrier of ((Y1 union Y2) union Y) by A87, Def2;

                hence thesis by A51, A84, A89, A90, Th4, Th5;

              end;

            end;

            take Y1, Y2;

            Y1 meets (X1 union X2) by A69, A79, A77;

            then the carrier of (Y1 meet (X1 union X2)) = (C1 /\ (A1 \/ A2)) by A79, A77, Def4;

            hence thesis by A59, A60, A78, A81, Th4;

          end;

        end;

        hence X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be open non empty SubSpace of X st (Y1 meet (X1 union X2)) is SubSpace of X1 & (Y2 meet (X1 union X2)) is SubSpace of X2 & ((X1 union X2) is SubSpace of (Y1 union Y2) or ex Y be closed non empty SubSpace of X st the TopStruct of X = ((Y1 union Y2) union Y) & (Y meet (X1 union X2)) is SubSpace of (X1 meet X2));

      end;

      hence thesis by A3;

    end;

    theorem :: TSEP_1:90

    X = (X1 union X2) & X1 meets X2 implies ((X1,X2) are_weakly_separated iff (X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be open non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be closed non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2))))

    proof

      reconsider A2 = the carrier of X2 as Subset of X by Th1;

      reconsider A1 = the carrier of X1 as Subset of X by Th1;

      assume

       A1: X = (X1 union X2);

      then

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

      assume

       A3: X1 meets X2;

       A4:

      now

        assume

         A5: X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be open non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be closed non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2));

        now

          assume ( not X1 is SubSpace of X2) & not X2 is SubSpace of X1;

          then

          consider Y1,Y2 be open non empty SubSpace of X such that

           A6: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and

           A7: X = (Y1 union Y2) or ex Y be closed non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2) by A5;

          reconsider C2 = the carrier of Y2 as Subset of X by Th1;

          reconsider C1 = the carrier of Y1 as Subset of X by Th1;

           A8:

          now

            per cases ;

              suppose

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

              thus ex C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is closed

              proof

                take ( {} X);

                thus thesis by A9, XBOOLE_1: 2;

              end;

            end;

              suppose

               A10: (A1 \/ A2) <> (C1 \/ C2);

              thus ex C be Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is closed

              proof

                consider Y be closed non empty SubSpace of X such that

                 A11: X = ((Y1 union Y2) union Y) and

                 A12: Y is SubSpace of (X1 meet X2) by A2, A7, A10, Def2;

                reconsider C = the carrier of Y as Subset of X by Th1;

                (A1 /\ A2) = the carrier of (X1 meet X2) by A3, Def4;

                then

                 A13: C c= (A1 /\ A2) by A12, Th4;



                 A14: C is closed by Th11;

                (A1 \/ A2) = (the carrier of (Y1 union Y2) \/ C) by A2, A11, Def2

                .= ((C1 \/ C2) \/ C) by Def2;

                hence thesis by A14, A13;

              end;

            end;

          end;



           A15: C1 is open & C2 is open by Th16;

          C1 c= A1 & C2 c= A2 by A6, Th4;

          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 A2, A15, A8, Th60;

          hence (X1,X2) are_weakly_separated ;

        end;

        hence (X1,X2) are_weakly_separated by Th79;

      end;

      now

        assume (X1,X2) are_weakly_separated ;

        then

         A16: (A1,A2) are_weakly_separated ;

        now

          assume ( not X1 is SubSpace of X2) & not X2 is SubSpace of X1;

          then ( not A1 c= A2) & not A2 c= A1 by Th4;

          then

          consider C1,C2 be non empty Subset of X such that

           A17: C1 is open and

           A18: C2 is open and

           A19: C1 c= A1 & C2 c= A2 and

           A20: (A1 \/ A2) = (C1 \/ C2) or ex C be non empty Subset of X st (A1 \/ A2) = ((C1 \/ C2) \/ C) & C c= (A1 /\ A2) & C is closed by A2, A16, Th61;

          thus ex Y1,Y2 be open non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be closed non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2))

          proof

            consider Y2 be strict open non empty SubSpace of X such that

             A21: C2 = the carrier of Y2 by A18, Th20;

            consider Y1 be strict open non empty SubSpace of X such that

             A22: C1 = the carrier of Y1 by A17, Th20;

            take Y1, Y2;

            now

              assume X <> (Y1 union Y2);

              then

              consider C be non empty Subset of X such that

               A23: (A1 \/ A2) = ((C1 \/ C2) \/ C) and

               A24: C c= (A1 /\ A2) and

               A25: C is closed by A1, A2, A20, A22, A21, Def2;

              thus ex Y be closed non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2)

              proof



                 A26: C c= the carrier of (X1 meet X2) by A3, A24, Def4;

                consider Y be strict closed non empty SubSpace of X such that

                 A27: C = the carrier of Y by A25, Th15;

                take Y;

                the carrier of X = (the carrier of (Y1 union Y2) \/ C) by A2, A22, A21, A23, Def2

                .= the carrier of ((Y1 union Y2) union Y) by A27, Def2;

                hence thesis by A1, A27, A26, Th4, Th5;

              end;

            end;

            hence thesis by A19, A22, A21, Th4;

          end;

        end;

        hence X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1,Y2 be open non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & (X = (Y1 union Y2) or ex Y be closed non empty SubSpace of X st X = ((Y1 union Y2) union Y) & Y is SubSpace of (X1 meet X2));

      end;

      hence thesis by A4;

    end;

    theorem :: TSEP_1:91

    X = (X1 union X2) & X1 misses X2 implies ((X1,X2) are_weakly_separated iff X1 is open SubSpace of X & X2 is open SubSpace of X)

    proof

      assume

       A1: X = (X1 union X2);

      assume

       A2: X1 misses X2;

      thus (X1,X2) are_weakly_separated implies X1 is open SubSpace of X & X2 is open SubSpace of X

      proof

        reconsider A2 = the carrier of X2 as Subset of X by Th1;

        reconsider A1 = the carrier of X1 as Subset of X by Th1;

        assume (X1,X2) are_weakly_separated ;

        then (X1,X2) are_separated by A2, Th78;

        then

         A3: (A1,A2) are_separated ;

        (A1 \/ A2) = ( [#] X) by A1, Def2;

        then A1 is open & A2 is open by A3, CONNSP_1: 4;

        hence thesis by Th16;

      end;

      thus thesis by Th81;

    end;

    theorem :: TSEP_1:92

    (X1,X2) are_separated iff ex Y1,Y2 be non empty SubSpace of X st (Y1,Y2) are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2))

    proof

      thus (X1,X2) are_separated implies ex Y1,Y2 be non empty SubSpace of X st (Y1,Y2) are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2))

      proof

        assume (X1,X2) are_separated ;

        then

        consider Y1,Y2 be open non empty SubSpace of X such that

         A1: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & (Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2)) by Th77;

        take Y1, Y2;

        thus thesis by A1, Th81;

      end;

      given Y1,Y2 be non empty SubSpace of X such that

       A2: (Y1,Y2) are_weakly_separated and

       A3: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and

       A4: Y1 misses Y2 or (Y1 meet Y2) misses (X1 union X2);

      reconsider C2 = the carrier of Y2 as Subset of X by Th1;

      reconsider C1 = the carrier of Y1 as Subset of X by Th1;

      now

        let A1,A2 be Subset of X such that

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

        now

          per cases ;

            suppose Y1 misses Y2;

            then (Y1,Y2) are_separated by A2, Th78;

            then

             A6: (C1,C2) are_separated ;

            A1 c= C1 & A2 c= C2 by A3, A5, Th4;

            hence (A1,A2) are_separated by A6, CONNSP_1: 7;

          end;

            suppose

             A7: not Y1 misses Y2;

            ex B1,B2 be Subset of X st (B1,B2) are_weakly_separated & A1 c= B1 & A2 c= B2 & (B1 /\ B2) misses (A1 \/ A2)

            proof

              take C1, C2;

              the carrier of (Y1 meet Y2) = (C1 /\ C2) & the carrier of (X1 union X2) = (A1 \/ A2) by A5, A7, Def2, Def4;

              hence thesis by A2, A3, A4, A5, A7, Th4;

            end;

            hence (A1,A2) are_separated by Th62;

          end;

        end;

        hence (A1,A2) are_separated ;

      end;

      hence thesis;

    end;

    theorem :: TSEP_1:93

    for T be TopStruct holds (T | ( [#] T)) = the TopStruct of T

    proof

      let T be TopStruct;

       the TopStruct of T is strict SubSpace of T & the carrier of T = ( [#] the TopStruct of T) by Th2, PRE_TOPC: 10;

      hence thesis by PRE_TOPC:def 5;

    end;