yellow12.miz



    begin

    reserve A,B,X,Y for set;

    registration

      let X be empty set;

      cluster ( union X) -> empty;

      coherence by ZFMISC_1: 2;

    end

     Lm1:

    now

      let S,T,x1,x2 be set such that

       A1: x1 in S & x2 in T;

      

       A2: ( dom <:( pr2 (S,T)), ( pr1 (S,T)):>) = (( dom ( pr2 (S,T))) /\ ( dom ( pr1 (S,T)))) by FUNCT_3:def 7

      .= (( dom ( pr2 (S,T))) /\ [:S, T:]) by FUNCT_3:def 4

      .= ( [:S, T:] /\ [:S, T:]) by FUNCT_3:def 5

      .= [:S, T:];

       [x1, x2] in [:S, T:] by A1, ZFMISC_1: 87;

      

      hence ( <:( pr2 (S,T)), ( pr1 (S,T)):> . (x1,x2)) = [(( pr2 (S,T)) . (x1,x2)), (( pr1 (S,T)) . (x1,x2))] by A2, FUNCT_3:def 7

      .= [x2, (( pr1 (S,T)) . (x1,x2))] by A1, FUNCT_3:def 5

      .= [x2, x1] by A1, FUNCT_3:def 4;

    end;

    theorem :: YELLOW12:1

    (( delta X) .: A) c= [:A, A:]

    proof

      set f = ( delta X);

      let y be object;

      assume y in (f .: A);

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: x in A and

       A3: y = (f . x) by FUNCT_1:def 6;

      y = [x, x] by A1, A3, FUNCT_3:def 6;

      hence thesis by A2, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW12:2

    

     Th2: (( delta X) " [:A, A:]) c= A

    proof

      set f = ( delta X);

      let x be object;

      assume x in (f " [:A, A:]);

      then (f . x) in [:A, A:] & (f . x) = [x, x] by FUNCT_1:def 7, FUNCT_3:def 6;

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: YELLOW12:3

    for A be Subset of X holds (( delta X) " [:A, A:]) = A

    proof

      let A be Subset of X;

      set f = ( delta X);

      thus (f " [:A, A:]) c= A by Th2;

      let x be object;

      assume

       A1: x in A;

      then (f . x) = [x, x] by FUNCT_3:def 6;

      then ( dom f) = X & (f . x) in [:A, A:] by A1, FUNCT_3:def 6, ZFMISC_1: 87;

      hence thesis by A1, FUNCT_1:def 7;

    end;

    theorem :: YELLOW12:4

    

     Th4: ( dom <:( pr2 (X,Y)), ( pr1 (X,Y)):>) = [:X, Y:] & ( rng <:( pr2 (X,Y)), ( pr1 (X,Y)):>) = [:Y, X:]

    proof

      set f = <:( pr2 (X,Y)), ( pr1 (X,Y)):>;

      

      thus

       A1: ( dom f) = (( dom ( pr2 (X,Y))) /\ ( dom ( pr1 (X,Y)))) by FUNCT_3:def 7

      .= (( dom ( pr2 (X,Y))) /\ [:X, Y:]) by FUNCT_3:def 4

      .= ( [:X, Y:] /\ [:X, Y:]) by FUNCT_3:def 5

      .= [:X, Y:];

      ( rng f) c= [:( rng ( pr2 (X,Y))), ( rng ( pr1 (X,Y))):] by FUNCT_3: 51;

      hence ( rng f) c= [:Y, X:] by XBOOLE_1: 1;

      let y be object;

      assume y in [:Y, X:];

      then

      consider y1,y2 be object such that

       A2: y1 in Y & y2 in X and

       A3: y = [y1, y2] by ZFMISC_1:def 2;

      

       A4: [y2, y1] in ( dom f) by A1, A2, ZFMISC_1: 87;

      (f . (y2,y1)) = y by A2, A3, Lm1;

      hence thesis by A4, FUNCT_1:def 3;

    end;

    theorem :: YELLOW12:5

    

     Th5: ( <:( pr2 (X,Y)), ( pr1 (X,Y)):> .: [:A, B:]) c= [:B, A:]

    proof

      set f = <:( pr2 (X,Y)), ( pr1 (X,Y)):>;

      let y be object;

      assume y in (f .: [:A, B:]);

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: x in [:A, B:] and

       A3: y = (f . x) by FUNCT_1:def 6;

      consider x1,x2 be object such that

       A4: x1 in A & x2 in B and

       A5: x = [x1, x2] by A2, ZFMISC_1:def 2;

      ( dom f) = [:X, Y:] by Th4;

      then x1 in X & x2 in Y by A1, A5, ZFMISC_1: 87;

      then (f . (x1,x2)) = [x2, x1] by Lm1;

      hence thesis by A3, A4, A5, ZFMISC_1: 87;

    end;

    theorem :: YELLOW12:6

    for A be Subset of X, B be Subset of Y holds ( <:( pr2 (X,Y)), ( pr1 (X,Y)):> .: [:A, B:]) = [:B, A:]

    proof

      let A be Subset of X, B be Subset of Y;

      set f = <:( pr2 (X,Y)), ( pr1 (X,Y)):>;

      

       A1: ( dom f) = [:X, Y:] by Th4;

      thus (f .: [:A, B:]) c= [:B, A:] by Th5;

      let y be object;

      assume y in [:B, A:];

      then

      consider y1,y2 be object such that

       A2: y1 in B & y2 in A and

       A3: y = [y1, y2] by ZFMISC_1:def 2;

       [y2, y1] in [:A, B:] & (f . (y2,y1)) = [y1, y2] by A2, Lm1, ZFMISC_1: 87;

      hence thesis by A1, A3, FUNCT_1:def 6;

    end;

    theorem :: YELLOW12:7

    

     Th7: <:( pr2 (X,Y)), ( pr1 (X,Y)):> is one-to-one

    proof

      set f = <:( pr2 (X,Y)), ( pr1 (X,Y)):>;

      let x,y be object such that

       A1: x in ( dom f) and

       A2: y in ( dom f) and

       A3: (f . x) = (f . y);

      

       A4: ( dom f) = [:X, Y:] by Th4;

      then

      consider x1,x2 be object such that

       A5: x1 in X & x2 in Y and

       A6: x = [x1, x2] by A1, ZFMISC_1:def 2;

      consider y1,y2 be object such that

       A7: y1 in X & y2 in Y and

       A8: y = [y1, y2] by A4, A2, ZFMISC_1:def 2;

      

       A9: (f . (y1,y2)) = [y2, y1] by A7, Lm1;

      

       A10: (f . (x1,x2)) = [x2, x1] by A5, Lm1;

      then x1 = y1 by A3, A6, A8, A9, XTUPLE_0: 1;

      hence thesis by A3, A6, A8, A10, A9, XTUPLE_0: 1;

    end;

    registration

      let X,Y be set;

      cluster <:( pr2 (X,Y)), ( pr1 (X,Y)):> -> one-to-one;

      coherence by Th7;

    end

    theorem :: YELLOW12:8

    

     Th8: ( <:( pr2 (X,Y)), ( pr1 (X,Y)):> " ) = <:( pr2 (Y,X)), ( pr1 (Y,X)):>

    proof

      set f = <:( pr2 (X,Y)), ( pr1 (X,Y)):>, g = <:( pr2 (Y,X)), ( pr1 (Y,X)):>;

      

       A1: ( dom (f " )) = ( rng f) by FUNCT_1: 32

      .= [:Y, X:] by Th4;

       A2:

      now

        let x be object;

        assume x in [:Y, X:];

        then

        consider x1,x2 be object such that

         A3: x1 in Y & x2 in X and

         A4: x = [x1, x2] by ZFMISC_1:def 2;

        

         A5: (g . (x1,x2)) = [x2, x1] & (f . (x2,x1)) = [x1, x2] by A3, Lm1;

        ( dom f) = [:X, Y:] by Th4;

        then [x2, x1] in ( dom f) by A3, ZFMISC_1: 87;

        hence ((f " ) . x) = (g . x) by A4, A5, FUNCT_1: 32;

      end;

      ( dom g) = [:Y, X:] by Th4;

      hence thesis by A1, A2;

    end;

    begin

    theorem :: YELLOW12:9

    

     Th9: for L1 be Semilattice, L2 be non empty RelStr holds for x,y be Element of L1, x1,y1 be Element of L2 st the RelStr of L1 = the RelStr of L2 & x = x1 & y = y1 holds (x "/\" y) = (x1 "/\" y1)

    proof

      let L1 be Semilattice, L2 be non empty RelStr, x,y be Element of L1, x1,y1 be Element of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: x = x1 & y = y1;

      

       A3: L2 is with_infima Poset by A1, WAYBEL_8: 12, WAYBEL_8: 13, WAYBEL_8: 14, YELLOW_7: 14;

      

       A4: ex_inf_of ( {x, y},L1) by YELLOW_0: 21;

      

      thus (x "/\" y) = ( inf {x, y}) by YELLOW_0: 40

      .= ( inf {x1, y1}) by A1, A2, A4, YELLOW_0: 27

      .= (x1 "/\" y1) by A3, YELLOW_0: 40;

    end;

    theorem :: YELLOW12:10

    

     Th10: for L1 be sup-Semilattice, L2 be non empty RelStr holds for x,y be Element of L1, x1,y1 be Element of L2 st the RelStr of L1 = the RelStr of L2 & x = x1 & y = y1 holds (x "\/" y) = (x1 "\/" y1)

    proof

      let L1 be sup-Semilattice, L2 be non empty RelStr, x,y be Element of L1, x1,y1 be Element of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: x = x1 & y = y1;

      

       A3: L2 is with_suprema Poset by A1, WAYBEL_8: 12, WAYBEL_8: 13, WAYBEL_8: 14, YELLOW_7: 15;

      

       A4: ex_sup_of ( {x, y},L1) by YELLOW_0: 20;

      

      thus (x "\/" y) = ( sup {x, y}) by YELLOW_0: 41

      .= ( sup {x1, y1}) by A1, A2, A4, YELLOW_0: 26

      .= (x1 "\/" y1) by A3, YELLOW_0: 41;

    end;

    theorem :: YELLOW12:11

    

     Th11: for L1 be Semilattice, L2 be non empty RelStr holds for X,Y be Subset of L1, X1,Y1 be Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = X1 & Y = Y1 holds (X "/\" Y) = (X1 "/\" Y1)

    proof

      let L1 be Semilattice, L2 be non empty RelStr, X,Y be Subset of L1, X1,Y1 be Subset of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: X = X1 & Y = Y1;

      set XY = { (x "/\" y) where x,y be Element of L1 : x in X & y in Y }, XY1 = { (x "/\" y) where x,y be Element of L2 : x in X1 & y in Y1 };

      

       A3: XY = XY1

      proof

        hereby

          let a be object;

          assume a in XY;

          then

          consider x,y be Element of L1 such that

           A4: a = (x "/\" y) and

           A5: x in X & y in Y;

          reconsider x1 = x, y1 = y as Element of L2 by A1;

          a = (x1 "/\" y1) by A1, A4, Th9;

          hence a in XY1 by A2, A5;

        end;

        let a be object;

        assume a in XY1;

        then

        consider x,y be Element of L2 such that

         A6: a = (x "/\" y) and

         A7: x in X1 & y in Y1;

        reconsider x1 = x, y1 = y as Element of L1 by A1;

        a = (x1 "/\" y1) by A1, A6, Th9;

        hence thesis by A2, A7;

      end;

      

      thus (X "/\" Y) = XY by YELLOW_4:def 4

      .= (X1 "/\" Y1) by A3, YELLOW_4:def 4;

    end;

    theorem :: YELLOW12:12

    for L1 be sup-Semilattice, L2 be non empty RelStr holds for X,Y be Subset of L1, X1,Y1 be Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = X1 & Y = Y1 holds (X "\/" Y) = (X1 "\/" Y1)

    proof

      let L1 be sup-Semilattice, L2 be non empty RelStr, X,Y be Subset of L1, X1,Y1 be Subset of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: X = X1 & Y = Y1;

      set XY = { (x "\/" y) where x,y be Element of L1 : x in X & y in Y }, XY1 = { (x "\/" y) where x,y be Element of L2 : x in X1 & y in Y1 };

      

       A3: XY = XY1

      proof

        hereby

          let a be object;

          assume a in XY;

          then

          consider x,y be Element of L1 such that

           A4: a = (x "\/" y) and

           A5: x in X & y in Y;

          reconsider x1 = x, y1 = y as Element of L2 by A1;

          a = (x1 "\/" y1) by A1, A4, Th10;

          hence a in XY1 by A2, A5;

        end;

        let a be object;

        assume a in XY1;

        then

        consider x,y be Element of L2 such that

         A6: a = (x "\/" y) and

         A7: x in X1 & y in Y1;

        reconsider x1 = x, y1 = y as Element of L1 by A1;

        a = (x1 "\/" y1) by A1, A6, Th10;

        hence thesis by A2, A7;

      end;

      

      thus (X "\/" Y) = XY by YELLOW_4:def 3

      .= (X1 "\/" Y1) by A3, YELLOW_4:def 3;

    end;

    theorem :: YELLOW12:13

    

     Th13: for L1 be antisymmetric up-complete non empty reflexive RelStr, L2 be non empty reflexive RelStr, x be Element of L1, y be Element of L2 st the RelStr of L1 = the RelStr of L2 & x = y holds ( waybelow x) = ( waybelow y) & ( wayabove x) = ( wayabove y)

    proof

      let L1 be antisymmetric up-complete non empty reflexive RelStr, L2 be non empty reflexive RelStr, x be Element of L1, y be Element of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: x = y;

      hereby

        hereby

          let a be object;

          assume a in ( waybelow x);

          then

          consider z be Element of L1 such that

           A3: a = z and

           A4: z << x;

          reconsider w = z as Element of L2 by A1;

          L2 is antisymmetric by A1, WAYBEL_8: 14;

          then w << y by A1, A2, A4, WAYBEL_8: 8;

          hence a in ( waybelow y) by A3;

        end;

        let a be object;

        assume a in ( waybelow y);

        then

        consider z be Element of L2 such that

         A5: a = z and

         A6: z << y;

        reconsider w = z as Element of L1 by A1;

        L2 is up-complete antisymmetric by A1, WAYBEL_8: 14, WAYBEL_8: 15;

        then w << x by A1, A2, A6, WAYBEL_8: 8;

        hence a in ( waybelow x) by A5;

      end;

      hereby

        let a be object;

        assume a in ( wayabove x);

        then

        consider z be Element of L1 such that

         A7: a = z and

         A8: z >> x;

        reconsider w = z as Element of L2 by A1;

        L2 is antisymmetric by A1, WAYBEL_8: 14;

        then w >> y by A1, A2, A8, WAYBEL_8: 8;

        hence a in ( wayabove y) by A7;

      end;

      let a be object;

      assume a in ( wayabove y);

      then

      consider z be Element of L2 such that

       A9: a = z and

       A10: z >> y;

      reconsider w = z as Element of L1 by A1;

      L2 is up-complete antisymmetric by A1, WAYBEL_8: 14, WAYBEL_8: 15;

      then w >> x by A1, A2, A10, WAYBEL_8: 8;

      hence thesis by A9;

    end;

    theorem :: YELLOW12:14

    for L1 be meet-continuous Semilattice, L2 be non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 holds L2 is meet-continuous

    proof

      let L1 be meet-continuous Semilattice, L2 be non empty reflexive RelStr;

      assume

       A1: the RelStr of L1 = the RelStr of L2;

      hence L2 is up-complete by WAYBEL_8: 15;

      let x be Element of L2, D be non empty directed Subset of L2;

      reconsider E = D as non empty directed Subset of L1 by A1, WAYBEL_0: 3;

      reconsider y = x as Element of L1 by A1;

      

       A2: ( {x} "/\" D) = ( {y} "/\" E) by A1, Th11;

      reconsider yy = {y} as non empty directed Subset of L1 by WAYBEL_0: 5;

      

       A3: ex_sup_of ((yy "/\" E),L1) by WAYBEL_0: 75;

       ex_sup_of (E,L1) by WAYBEL_0: 75;

      then ( sup D) = ( sup E) by A1, YELLOW_0: 26;

      

      hence (x "/\" ( sup D)) = (y "/\" ( sup E)) by A1, Th9

      .= ( sup ( {y} "/\" E)) by WAYBEL_2:def 6

      .= ( sup ( {x} "/\" D)) by A1, A2, A3, YELLOW_0: 26;

    end;

    theorem :: YELLOW12:15

    for L1 be continuous antisymmetric non empty reflexive RelStr, L2 be non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 holds L2 is continuous

    proof

      let L1 be continuous antisymmetric non empty reflexive RelStr, L2 be non empty reflexive RelStr such that

       A1: the RelStr of L1 = the RelStr of L2;

      hereby

        let y be Element of L2;

        reconsider x = y as Element of L1 by A1;

        ( waybelow x) = ( waybelow y) by A1, Th13;

        hence ( waybelow y) is non empty directed by A1, WAYBEL_0: 3;

      end;

      thus L2 is up-complete by A1, WAYBEL_8: 15;

      let y be Element of L2;

      reconsider x = y as Element of L1 by A1;

      

       A2: ex_sup_of (( waybelow x),L1) & x = ( sup ( waybelow x)) by WAYBEL_0: 75, WAYBEL_3:def 5;

      ( waybelow x) = ( waybelow y) by A1, Th13;

      hence thesis by A1, A2, YELLOW_0: 26;

    end;

    theorem :: YELLOW12:16

    for L1,L2 be RelStr, A be Subset of L1, J be Subset of L2 st the RelStr of L1 = the RelStr of L2 & A = J holds ( subrelstr A) = ( subrelstr J)

    proof

      let L1,L2 be RelStr, A be Subset of L1, J be Subset of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: A = J;

      

       A3: the carrier of ( subrelstr A) = A by YELLOW_0:def 15

      .= the carrier of ( subrelstr J) by A2, YELLOW_0:def 15;

      

      then the InternalRel of ( subrelstr A) = (the InternalRel of L2 |_2 the carrier of ( subrelstr J)) by A1, YELLOW_0:def 14

      .= the InternalRel of ( subrelstr J) by YELLOW_0:def 14;

      hence thesis by A3;

    end;

    theorem :: YELLOW12:17

    for L1,L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the RelStr of J & A is meet-inheriting holds J is meet-inheriting

    proof

      let L1,L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: the RelStr of A = the RelStr of J and

       A3: for x,y be Element of L1 st x in the carrier of A & y in the carrier of A & ex_inf_of ( {x, y},L1) holds ( inf {x, y}) in the carrier of A;

      let x,y be Element of L2 such that

       A4: x in the carrier of J & y in the carrier of J and

       A5: ex_inf_of ( {x, y},L2);

      reconsider x1 = x, y1 = y as Element of L1 by A1;

      ( inf {x1, y1}) in the carrier of A by A1, A2, A3, A4, A5, YELLOW_0: 14;

      hence thesis by A1, A2, A5, YELLOW_0: 27;

    end;

    theorem :: YELLOW12:18

    for L1,L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2 st the RelStr of L1 = the RelStr of L2 & the RelStr of A = the RelStr of J & A is join-inheriting holds J is join-inheriting

    proof

      let L1,L2 be non empty RelStr, A be SubRelStr of L1, J be SubRelStr of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: the RelStr of A = the RelStr of J and

       A3: for x,y be Element of L1 st x in the carrier of A & y in the carrier of A & ex_sup_of ( {x, y},L1) holds ( sup {x, y}) in the carrier of A;

      let x,y be Element of L2 such that

       A4: x in the carrier of J & y in the carrier of J and

       A5: ex_sup_of ( {x, y},L2);

      reconsider x1 = x, y1 = y as Element of L1 by A1;

      ( sup {x1, y1}) in the carrier of A by A1, A2, A3, A4, A5, YELLOW_0: 14;

      hence thesis by A1, A2, A5, YELLOW_0: 26;

    end;

    theorem :: YELLOW12:19

    for L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = Y & X is property(S) holds Y is property(S)

    proof

      let L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: X = Y and

       A3: for D be non empty directed Subset of L1 st ( sup D) in X holds ex y be Element of L1 st y in D & for x be Element of L1 st x in D & x >= y holds x in X;

      let E be non empty directed Subset of L2 such that

       A4: ( sup E) in Y;

      reconsider D = E as non empty directed Subset of L1 by A1, WAYBEL_0: 3;

       ex_sup_of (D,L1) by WAYBEL_0: 75;

      then ( sup D) in X by A1, A2, A4, YELLOW_0: 26;

      then

      consider y be Element of L1 such that

       A5: y in D and

       A6: for x be Element of L1 st x in D & x >= y holds x in X by A3;

      reconsider y2 = y as Element of L2 by A1;

      take y2;

      thus y2 in E by A5;

      let x2 be Element of L2;

      assume x2 in E & x2 >= y2;

      hence thesis by A1, A2, A6, YELLOW_0: 1;

    end;

    theorem :: YELLOW12:20

    for L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 st the RelStr of L1 = the RelStr of L2 & X = Y & X is directly_closed holds Y is directly_closed

    proof

      let L1 be up-complete antisymmetric non empty reflexive RelStr, L2 be non empty reflexive RelStr, X be Subset of L1, Y be Subset of L2 such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: X = Y and

       A3: for D be non empty directed Subset of L1 st D c= X holds ( sup D) in X;

      let E be non empty directed Subset of L2 such that

       A4: E c= Y;

      reconsider D = E as non empty directed Subset of L1 by A1, WAYBEL_0: 3;

       ex_sup_of (D,L1) & ( sup D) in X by A2, A3, A4, WAYBEL_0: 75;

      hence thesis by A1, A2, YELLOW_0: 26;

    end;

    theorem :: YELLOW12:21

    for N be antisymmetric with_infima RelStr, D,E be Subset of N holds for X be upper Subset of N st D misses X holds (D "/\" E) misses X

    proof

      let N be antisymmetric with_infima RelStr, D,E be Subset of N, X be upper Subset of N such that

       A1: (D /\ X) = {} ;

      assume ((D "/\" E) /\ X) <> {} ;

      then

      consider k be object such that

       A2: k in ((D "/\" E) /\ X) by XBOOLE_0:def 1;

      reconsider k as Element of N by A2;

      

       A3: (D "/\" E) = { (d "/\" e) where d,e be Element of N : d in D & e in E } & k in (D "/\" E) by A2, XBOOLE_0:def 4, YELLOW_4:def 4;

      

       A4: k in X by A2, XBOOLE_0:def 4;

      consider d,e be Element of N such that

       A5: k = (d "/\" e) and

       A6: d in D and e in E by A3;

      (d "/\" e) <= d by YELLOW_0: 23;

      then d in X by A4, A5, WAYBEL_0:def 20;

      hence thesis by A1, A6, XBOOLE_0:def 4;

    end;

    theorem :: YELLOW12:22

    for R be reflexive non empty RelStr holds ( id the carrier of R) c= (the InternalRel of R /\ the InternalRel of (R ~ ))

    proof

      let R be reflexive non empty RelStr;

      let a be object;

      assume

       A1: a in ( id the carrier of R);

      then

      consider y,z be object such that

       A2: a = [y, z] by RELAT_1:def 1;

      reconsider y, z as Element of R by A1, A2, ZFMISC_1: 87;

      y <= z by A1, A2, RELAT_1:def 10;

      then

       A3: a in the InternalRel of R by A2, ORDERS_2:def 5;

      y = z by A1, A2, RELAT_1:def 10;

      then a in the InternalRel of (R ~ ) by A2, A3, RELAT_1:def 7;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    theorem :: YELLOW12:23

    for R be antisymmetric RelStr holds (the InternalRel of R /\ the InternalRel of (R ~ )) c= ( id the carrier of R)

    proof

      let R be antisymmetric RelStr;

      let a be object;

      assume

       A1: a in (the InternalRel of R /\ the InternalRel of (R ~ ));

      then

      consider y,z be object such that

       A2: a = [y, z] by RELAT_1:def 1;

      

       A3: y in the carrier of R by A1, A2, ZFMISC_1: 87;

      reconsider y, z as Element of R by A1, A2, ZFMISC_1: 87;

      a in the InternalRel of (R ~ ) by A1, XBOOLE_0:def 4;

      then [z, y] in the InternalRel of R by A2, RELAT_1:def 7;

      then

       A4: z <= y by ORDERS_2:def 5;

      a in the InternalRel of R by A1, XBOOLE_0:def 4;

      then y <= z by A2, ORDERS_2:def 5;

      then y = z by A4, ORDERS_2: 2;

      hence thesis by A2, A3, RELAT_1:def 10;

    end;

    definition

      let L be non empty RelStr;

      let f be Function of [:L, L:], L;

      let a,b be Element of L;

      :: original: .

      redefine

      func f . (a,b) -> Element of L ;

      coherence

      proof

        (f . [a, b]) is Element of L;

        hence thesis;

      end;

    end

    theorem :: YELLOW12:24

    

     Th24: for R be upper-bounded Semilattice, X be Subset of [:R, R:] st ex_inf_of ((( inf_op R) .: X),R) holds ( inf_op R) preserves_inf_of X

    proof

      let R be upper-bounded Semilattice;

      set f = ( inf_op R);

      let X be Subset of [:R, R:] such that

       A1: ex_inf_of ((f .: X),R) and

       A2: ex_inf_of (X, [:R, R:]);

      thus ex_inf_of ((f .: X),R) by A1;

      

       A3: ( dom f) = the carrier of [:R, R:] by FUNCT_2:def 1;

      then

       A4: ( dom f) = [:the carrier of R, the carrier of R:] by YELLOW_3:def 2;

      

       A5: for b be Element of R st b is_<=_than (f .: X) holds (f . ( inf X)) >= b

      proof

        let b be Element of R such that

         A6: b is_<=_than (f .: X);

        X is_>=_than [b, b]

        proof

          let c be Element of [:R, R:];

          assume c in X;

          then (f . c) in (f .: X) by A3, FUNCT_1:def 6;

          then

           A7: b <= (f . c) by A6;

          consider s,t be object such that

           A8: s in the carrier of R & t in the carrier of R and

           A9: c = [s, t] by A3, A4, ZFMISC_1:def 2;

          reconsider s, t as Element of R by A8;

          

           A10: (f . c) = (f . (s,t)) by A9

          .= (s "/\" t) by WAYBEL_2:def 4;

          (s "/\" t) <= t by YELLOW_0: 23;

          then

           A11: b <= t by A7, A10, ORDERS_2: 3;

          (s "/\" t) <= s by YELLOW_0: 23;

          then b <= s by A7, A10, ORDERS_2: 3;

          hence [b, b] <= c by A9, A11, YELLOW_3: 11;

        end;

        then [b, b] <= ( inf X) by A2, YELLOW_0:def 10;

        then (f . (b,b)) <= (f . ( inf X)) by WAYBEL_1:def 2;

        then (b "/\" b) <= (f . ( inf X)) by WAYBEL_2:def 4;

        hence b <= (f . ( inf X)) by YELLOW_0: 25;

      end;

      ( inf X) is_<=_than X by A2, YELLOW_0:def 10;

      then (f . ( inf X)) is_<=_than (f .: X) by YELLOW_2: 13;

      hence thesis by A1, A5, YELLOW_0:def 10;

    end;

    registration

      let R be complete Semilattice;

      cluster ( inf_op R) -> infs-preserving;

      coherence

      proof

        let X be Subset of [:R, R:] such that

         A1: ex_inf_of (X, [:R, R:]);

        thus ex_inf_of ((( inf_op R) .: X),R) by YELLOW_0: 17;

        then ( inf_op R) preserves_inf_of X by Th24;

        hence thesis by A1;

      end;

    end

    theorem :: YELLOW12:25

    

     Th25: for R be lower-bounded sup-Semilattice, X be Subset of [:R, R:] st ex_sup_of ((( sup_op R) .: X),R) holds ( sup_op R) preserves_sup_of X

    proof

      let R be lower-bounded sup-Semilattice;

      set f = ( sup_op R);

      let X be Subset of [:R, R:] such that

       A1: ex_sup_of ((f .: X),R) and

       A2: ex_sup_of (X, [:R, R:]);

      thus ex_sup_of ((f .: X),R) by A1;

      

       A3: ( dom f) = the carrier of [:R, R:] by FUNCT_2:def 1;

      then

       A4: ( dom f) = [:the carrier of R, the carrier of R:] by YELLOW_3:def 2;

      

       A5: for b be Element of R st b is_>=_than (f .: X) holds (f . ( sup X)) <= b

      proof

        let b be Element of R such that

         A6: b is_>=_than (f .: X);

        X is_<=_than [b, b]

        proof

          let c be Element of [:R, R:];

          assume c in X;

          then (f . c) in (f .: X) by A3, FUNCT_1:def 6;

          then

           A7: (f . c) <= b by A6;

          consider s,t be object such that

           A8: s in the carrier of R & t in the carrier of R and

           A9: c = [s, t] by A3, A4, ZFMISC_1:def 2;

          reconsider s, t as Element of R by A8;

          

           A10: (f . c) = (f . (s,t)) by A9

          .= (s "\/" t) by WAYBEL_2:def 5;

          t <= (s "\/" t) by YELLOW_0: 22;

          then

           A11: t <= b by A7, A10, ORDERS_2: 3;

          s <= (s "\/" t) by YELLOW_0: 22;

          then s <= b by A7, A10, ORDERS_2: 3;

          hence c <= [b, b] by A9, A11, YELLOW_3: 11;

        end;

        then ( sup X) <= [b, b] by A2, YELLOW_0:def 9;

        then (f . ( sup X)) <= (f . (b,b)) by WAYBEL_1:def 2;

        then b <= b & (f . ( sup X)) <= (b "\/" b) by WAYBEL_2:def 5;

        hence thesis by YELLOW_0: 24;

      end;

      X is_<=_than ( sup X) by A2, YELLOW_0:def 9;

      then (f .: X) is_<=_than (f . ( sup X)) by YELLOW_2: 14;

      hence thesis by A1, A5, YELLOW_0:def 9;

    end;

    registration

      let R be complete sup-Semilattice;

      cluster ( sup_op R) -> sups-preserving;

      coherence

      proof

        let X be Subset of [:R, R:] such that

         A1: ex_sup_of (X, [:R, R:]);

        thus ex_sup_of ((( sup_op R) .: X),R) by YELLOW_0: 17;

        then ( sup_op R) preserves_sup_of X by Th25;

        hence thesis by A1;

      end;

    end

    theorem :: YELLOW12:26

    for N be Semilattice, A be Subset of N st ( subrelstr A) is meet-inheriting holds A is filtered

    proof

      let N be Semilattice, A be Subset of N such that

       A1: ( subrelstr A) is meet-inheriting;

      let x,y be Element of N such that

       A2: x in A & y in A;

      take (x "/\" y);

      

       A3: the carrier of ( subrelstr A) = A by YELLOW_0:def 15;

       ex_inf_of ( {x, y},N) by YELLOW_0: 21;

      then ( inf {x, y}) in the carrier of ( subrelstr A) by A1, A2, A3;

      hence (x "/\" y) in A by A3, YELLOW_0: 40;

      thus (x "/\" y) <= x & (x "/\" y) <= y by YELLOW_0: 23;

    end;

    theorem :: YELLOW12:27

    for N be sup-Semilattice, A be Subset of N st ( subrelstr A) is join-inheriting holds A is directed

    proof

      let N be sup-Semilattice, A be Subset of N such that

       A1: ( subrelstr A) is join-inheriting;

      let x,y be Element of N such that

       A2: x in A & y in A;

      take (x "\/" y);

      

       A3: the carrier of ( subrelstr A) = A by YELLOW_0:def 15;

       ex_sup_of ( {x, y},N) by YELLOW_0: 20;

      then ( sup {x, y}) in the carrier of ( subrelstr A) by A1, A2, A3;

      hence (x "\/" y) in A by A3, YELLOW_0: 41;

      thus x <= (x "\/" y) & y <= (x "\/" y) by YELLOW_0: 22;

    end;

    theorem :: YELLOW12:28

    for N be transitive RelStr, A,J be Subset of N st A is_coarser_than ( uparrow J) holds ( uparrow A) c= ( uparrow J)

    proof

      let N be transitive RelStr, A,J be Subset of N such that

       A1: A is_coarser_than ( uparrow J);

      let w be object;

      assume

       A2: w in ( uparrow A);

      then

      reconsider w1 = w as Element of N;

      consider t be Element of N such that

       A3: t <= w1 and

       A4: t in A by A2, WAYBEL_0:def 16;

      consider t1 be Element of N such that

       A5: t1 in ( uparrow J) and

       A6: t1 <= t by A1, A4, YELLOW_4:def 2;

      consider t2 be Element of N such that

       A7: t2 <= t1 and

       A8: t2 in J by A5, WAYBEL_0:def 16;

      t2 <= t by A6, A7, ORDERS_2: 3;

      then t2 <= w1 by A3, ORDERS_2: 3;

      hence thesis by A8, WAYBEL_0:def 16;

    end;

    theorem :: YELLOW12:29

    for N be transitive RelStr, A,J be Subset of N st A is_finer_than ( downarrow J) holds ( downarrow A) c= ( downarrow J)

    proof

      let N be transitive RelStr, A,J be Subset of N such that

       A1: A is_finer_than ( downarrow J);

      let w be object;

      assume

       A2: w in ( downarrow A);

      then

      reconsider w1 = w as Element of N;

      consider t be Element of N such that

       A3: w1 <= t and

       A4: t in A by A2, WAYBEL_0:def 15;

      consider t1 be Element of N such that

       A5: t1 in ( downarrow J) and

       A6: t <= t1 by A1, A4, YELLOW_4:def 1;

      consider t2 be Element of N such that

       A7: t1 <= t2 and

       A8: t2 in J by A5, WAYBEL_0:def 15;

      w1 <= t1 by A3, A6, ORDERS_2: 3;

      then w1 <= t2 by A7, ORDERS_2: 3;

      hence thesis by A8, WAYBEL_0:def 15;

    end;

    theorem :: YELLOW12:30

    for N be non empty reflexive RelStr holds for x be Element of N, X be Subset of N st x in X holds ( uparrow x) c= ( uparrow X)

    proof

      let N be non empty reflexive RelStr, x be Element of N, X be Subset of N such that

       A1: x in X;

      let a be object;

      assume

       A2: a in ( uparrow x);

      then

      reconsider b = a as Element of N;

      x <= b by A2, WAYBEL_0: 18;

      hence thesis by A1, WAYBEL_0:def 16;

    end;

    theorem :: YELLOW12:31

    for N be non empty reflexive RelStr holds for x be Element of N, X be Subset of N st x in X holds ( downarrow x) c= ( downarrow X)

    proof

      let N be non empty reflexive RelStr, x be Element of N, X be Subset of N such that

       A1: x in X;

      let a be object;

      assume

       A2: a in ( downarrow x);

      then

      reconsider b = a as Element of N;

      b <= x by A2, WAYBEL_0: 17;

      hence thesis by A1, WAYBEL_0:def 15;

    end;

    begin

    reserve R,S,T for non empty TopSpace;

    theorem :: YELLOW12:32

    

     Th32: for S,T be TopStruct, B be Basis of S st the TopStruct of S = the TopStruct of T holds B is Basis of T

    proof

      let S,T be TopStruct, B be Basis of S;

      

       A1: B c= the topology of S by TOPS_2: 64;

      assume

       A2: the TopStruct of S = the TopStruct of T;

      then the topology of T c= ( UniCl B) by CANTOR_1:def 2;

      hence thesis by A2, A1, CANTOR_1:def 2, TOPS_2: 64;

    end;

    theorem :: YELLOW12:33

    

     Th33: for S,T be TopStruct, B be prebasis of S st the TopStruct of S = the TopStruct of T holds B is prebasis of T

    proof

      let S,T be TopStruct, B be prebasis of S;

      consider F be Basis of S such that

       A1: F c= ( FinMeetCl B) by CANTOR_1:def 4;

      assume

       A2: the TopStruct of S = the TopStruct of T;

      then B c= the topology of T & F is Basis of T by Th32, TOPS_2: 64;

      hence thesis by A2, A1, CANTOR_1:def 4, TOPS_2: 64;

    end;

    theorem :: YELLOW12:34

    

     Th34: for J be Basis of T holds J is non empty

    proof

      let J be Basis of T;

      assume J is empty;

      then

       A1: ( UniCl J) = { {} } by YELLOW_9: 16;

      the topology of T c= ( UniCl J) & the carrier of T in the topology of T by CANTOR_1:def 2, PRE_TOPC:def 1;

      hence contradiction by A1, TARSKI:def 1;

    end;

    registration

      let T be non empty TopSpace;

      cluster -> non empty for Basis of T;

      coherence by Th34;

    end

    theorem :: YELLOW12:35

    

     Th35: for x be Point of T, J be Basis of x holds J is non empty

    proof

      let x be Point of T, J be Basis of x;

      ex W be Subset of T st W in J & W c= ( [#] T) by YELLOW_8: 13;

      hence thesis;

    end;

    registration

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

      cluster -> non empty for Basis of x;

      coherence by Th35;

    end

    theorem :: YELLOW12:36

    for S1,T1,S2,T2 be TopSpace, f be Function of S1, S2, g be Function of T1, T2 st the TopStruct of S1 = the TopStruct of T1 & the TopStruct of S2 = the TopStruct of T2 & f = g & f is continuous holds g is continuous

    proof

      let S1,T1,S2,T2 be TopSpace, f be Function of S1, S2, g be Function of T1, T2 such that

       A1: the TopStruct of S1 = the TopStruct of T1 and

       A2: the TopStruct of S2 = the TopStruct of T2 and

       A3: f = g and

       A4: f is continuous;

      now

        let P2 be Subset of T2 such that

         A5: P2 is closed;

        reconsider P1 = P2 as Subset of S2 by A2;

        P1 is closed by A2, A5, TOPS_3: 79;

        then (f " P1) is closed by A4;

        hence (g " P2) is closed by A1, A3, TOPS_3: 79;

      end;

      hence thesis;

    end;

    theorem :: YELLOW12:37

    

     Th37: ( id the carrier of T) = { p where p be Point of [:T, T:] : (( pr1 (the carrier of T,the carrier of T)) . p) = (( pr2 (the carrier of T,the carrier of T)) . p) }

    proof

      set f = ( pr1 (the carrier of T,the carrier of T)), g = ( pr2 (the carrier of T,the carrier of T));

      

       A1: the carrier of [:T, T:] = [:the carrier of T, the carrier of T:] by BORSUK_1:def 2;

      hereby

        let a be object;

        assume

         A2: a in ( id the carrier of T);

        then

        consider x,y be object such that

         A3: x in the carrier of T and

         A4: y in the carrier of T and

         A5: a = [x, y] by ZFMISC_1:def 2;

        

         A6: x = y by A2, A5, RELAT_1:def 10;

        (f . (x,y)) = x by A3, A4, FUNCT_3:def 4

        .= (g . (x,y)) by A3, A6, FUNCT_3:def 5;

        hence a in { p where p be Point of [:T, T:] : (f . p) = (g . p) } by A1, A2, A5;

      end;

      let a be object;

      assume a in { p where p be Point of [:T, T:] : (f . p) = (g . p) };

      then

      consider p be Point of [:T, T:] such that

       A7: a = p and

       A8: (f . p) = (g . p);

      consider x,y be object such that

       A9: x in the carrier of T and

       A10: y in the carrier of T and

       A11: p = [x, y] by A1, ZFMISC_1:def 2;

      

       A12: (f . (x,y)) = (g . (x,y)) by A8, A11;

      x = (f . (x,y)) by A9, A10, FUNCT_3:def 4

      .= y by A9, A10, A12, FUNCT_3:def 5;

      hence thesis by A7, A9, A11, RELAT_1:def 10;

    end;

    theorem :: YELLOW12:38

    

     Th38: ( delta the carrier of T) is continuous Function of T, [:T, T:]

    proof

      the carrier of [:T, T:] = [:the carrier of T, the carrier of T:] by BORSUK_1:def 2;

      then

      reconsider f = ( delta the carrier of T) as Function of T, [:T, T:];

      f is continuous

      proof

        let W be Point of T, G be a_neighborhood of (f . W);

        consider A be Subset-Family of [:T, T:] such that

         A1: ( Int G) = ( union A) and

         A2: for e be set st e in A holds ex X1,Y1 be Subset of T st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

        (f . W) in ( Int G) by CONNSP_2:def 1;

        then

        consider Z be set such that

         A3: (f . W) in Z and

         A4: Z in A by A1, TARSKI:def 4;

        consider X1,Y1 be Subset of T such that

         A5: Z = [:X1, Y1:] and

         A6: X1 is open & Y1 is open by A2, A4;

        (f . W) = [W, W] by FUNCT_3:def 6;

        then W in X1 & W in Y1 by A3, A5, ZFMISC_1: 87;

        then

         A7: W in (X1 /\ Y1) by XBOOLE_0:def 4;

        (X1 /\ Y1) is open by A6;

        then W in ( Int (X1 /\ Y1)) by A7, TOPS_1: 23;

        then

        reconsider H = (X1 /\ Y1) as a_neighborhood of W by CONNSP_2:def 1;

        

         A8: (f .: H) c= ( Int G)

        proof

          let y be object;

          assume y in (f .: H);

          then

          consider x be object such that

           A9: x in ( dom f) and

           A10: x in H and

           A11: y = (f . x) by FUNCT_1:def 6;

          

           A12: x in X1 & x in Y1 by A10, XBOOLE_0:def 4;

          y = [x, x] by A9, A11, FUNCT_3:def 6;

          then y in Z by A5, A12, ZFMISC_1: 87;

          hence thesis by A1, A4, TARSKI:def 4;

        end;

        take H;

        ( Int G) c= G by TOPS_1: 16;

        hence thesis by A8;

      end;

      hence thesis;

    end;

    theorem :: YELLOW12:39

    

     Th39: ( pr1 (the carrier of S,the carrier of T)) is continuous Function of [:S, T:], S

    proof

      set I = the carrier of S, J = the carrier of T;

      

       A1: the carrier of [:S, T:] = [:I, J:] by BORSUK_1:def 2;

      then

      reconsider f = ( pr1 (I,J)) as Function of [:S, T:], S;

      f is continuous

      proof

        let w be Point of [:S, T:], G be a_neighborhood of (f . w);

        set H = [:( Int G), ( [#] T):];

        

         A2: ( Int H) = [:( Int ( Int G)), ( Int ( [#] T)):] by BORSUK_1: 7

        .= [:( Int G), ( [#] T):] by TOPS_1: 15;

        consider x,y be object such that

         A3: x in I and

         A4: y in J and

         A5: w = [x, y] by A1, ZFMISC_1:def 2;

        (f . w) in ( Int G) & (f . (x,y)) = x by A3, A4, CONNSP_2:def 1, FUNCT_3:def 4;

        then w in ( Int H) by A4, A5, A2, ZFMISC_1:def 2;

        then

        reconsider H as a_neighborhood of w by CONNSP_2:def 1;

        take H;

        reconsider X = ( Int G) as non empty Subset of S by CONNSP_2:def 1;

         [:X, ( [#] T):] <> {} ;

        then (f .: H) = ( Int G) by EQREL_1: 49;

        hence thesis by TOPS_1: 16;

      end;

      hence thesis;

    end;

    theorem :: YELLOW12:40

    

     Th40: ( pr2 (the carrier of S,the carrier of T)) is continuous Function of [:S, T:], T

    proof

      set I = the carrier of S, J = the carrier of T;

      

       A1: the carrier of [:S, T:] = [:I, J:] by BORSUK_1:def 2;

      then

      reconsider f = ( pr2 (I,J)) as Function of [:S, T:], T;

      f is continuous

      proof

        let w be Point of [:S, T:], G be a_neighborhood of (f . w);

        set H = [:( [#] S), ( Int G):];

        

         A2: ( Int H) = [:( Int ( [#] S)), ( Int ( Int G)):] by BORSUK_1: 7

        .= [:( [#] S), ( Int G):] by TOPS_1: 15;

        consider x,y be object such that

         A3: x in I and

         A4: y in J and

         A5: w = [x, y] by A1, ZFMISC_1:def 2;

        (f . w) in ( Int G) & (f . (x,y)) = y by A3, A4, CONNSP_2:def 1, FUNCT_3:def 5;

        then w in ( Int H) by A3, A5, A2, ZFMISC_1:def 2;

        then

        reconsider H as a_neighborhood of w by CONNSP_2:def 1;

        take H;

        reconsider X = ( Int G) as non empty Subset of T by CONNSP_2:def 1;

         [:( [#] S), X:] <> {} ;

        then (f .: H) = ( Int G) by EQREL_1: 49;

        hence thesis by TOPS_1: 16;

      end;

      hence thesis;

    end;

    theorem :: YELLOW12:41

    

     Th41: for f be continuous Function of T, S, g be continuous Function of T, R holds <:f, g:> is continuous Function of T, [:S, R:]

    proof

      let f be continuous Function of T, S, g be continuous Function of T, R;

      

       A1: <:f, g:> = ( [:f, g:] * ( delta the carrier of T)) by FUNCT_3: 78;

      ( delta the carrier of T) is continuous Function of T, [:T, T:] by Th38;

      hence thesis by A1;

    end;

    theorem :: YELLOW12:42

    

     Th42: <:( pr2 (the carrier of S,the carrier of T)), ( pr1 (the carrier of S,the carrier of T)):> is continuous Function of [:S, T:], [:T, S:]

    proof

      ( pr1 (the carrier of S,the carrier of T)) is continuous Function of [:S, T:], S & ( pr2 (the carrier of S,the carrier of T)) is continuous Function of [:S, T:], T by Th39, Th40;

      hence thesis by Th41;

    end;

    theorem :: YELLOW12:43

    

     Th43: for f be Function of [:S, T:], [:T, S:] st f = <:( pr2 (the carrier of S,the carrier of T)), ( pr1 (the carrier of S,the carrier of T)):> holds f is being_homeomorphism

    proof

      let f be Function of [:S, T:], [:T, S:] such that

       A1: f = <:( pr2 (the carrier of S,the carrier of T)), ( pr1 (the carrier of S,the carrier of T)):>;

      thus ( dom f) = ( [#] [:S, T:]) by FUNCT_2:def 1;

      

      thus

       A2: ( rng f) = [:the carrier of T, the carrier of S:] by A1, Th4

      .= ( [#] [:T, S:]) by BORSUK_1:def 2;

      thus f is one-to-one by A1;

      thus f is continuous by A1, Th42;

      f is onto by A2, FUNCT_2:def 3;

      

      then (f " ) = (f qua Function " ) by A1, TOPS_2:def 4

      .= <:( pr2 (the carrier of T,the carrier of S)), ( pr1 (the carrier of T,the carrier of S)):> by A1, Th8;

      hence thesis by Th42;

    end;

    theorem :: YELLOW12:44

    ( [:S, T:], [:T, S:]) are_homeomorphic

    proof

      reconsider f = <:( pr2 (the carrier of S,the carrier of T)), ( pr1 (the carrier of S,the carrier of T)):> as Function of [:S, T:], [:T, S:] by Th42;

      take f;

      thus thesis by Th43;

    end;

    theorem :: YELLOW12:45

    

     Th45: for T be Hausdorff non empty TopSpace holds for f,g be continuous Function of S, T holds (for X be Subset of S st X = { p where p be Point of S : (f . p) <> (g . p) } holds X is open) & for X be Subset of S st X = { p where p be Point of S : (f . p) = (g . p) } holds X is closed

    proof

      let T be Hausdorff non empty TopSpace, f,g be continuous Function of S, T;

      { p where p be Point of S : (f . p) <> (g . p) } c= the carrier of S

      proof

        let x be object;

        assume x in { p where p be Point of S : (f . p) <> (g . p) };

        then ex a be Point of S st x = a & (f . a) <> (g . a);

        hence thesis;

      end;

      then

      reconsider A = { p where p be Point of S : (f . p) <> (g . p) } as Subset of S;

      

       A1: ( [#] T) <> {} ;

      thus for X be Subset of S st X = { p where p be Point of S : (f . p) <> (g . p) } holds X is open

      proof

        let X be Subset of S such that

         A2: X = { p where p be Point of S : (f . p) <> (g . p) };

        for x be set holds x in X iff ex Q be Subset of S st Q is open & Q c= X & x in Q

        proof

          let x be set;

          hereby

            assume x in X;

            then

            consider p be Point of S such that

             A3: x = p and

             A4: (f . p) <> (g . p) by A2;

            consider W,V be Subset of T such that

             A5: W is open & V is open and

             A6: (f . p) in W and

             A7: (g . p) in V and

             A8: W misses V by A4, PRE_TOPC:def 10;

            ( dom g) = the carrier of S by FUNCT_2:def 1;

            then [x, (g . p)] in g by A3, FUNCT_1:def 2;

            then

             A9: x in (g " V) by A7, RELAT_1:def 14;

            take Q = ((f " W) /\ (g " V));

            (f " W) is open & (g " V) is open by A1, A5, TOPS_2: 43;

            hence Q is open;

            thus Q c= X

            proof

              let q be object;

              assume

               A10: q in Q;

              then q in (f " W) by XBOOLE_0:def 4;

              then

              consider yf be object such that

               A11: [q, yf] in f and

               A12: yf in W by RELAT_1:def 14;

              q in (g " V) by A10, XBOOLE_0:def 4;

              then

              consider yg be object such that

               A13: [q, yg] in g & yg in V by RELAT_1:def 14;

              

               A14: yg = (g . q) & not yg in W by A8, A13, FUNCT_1: 1, XBOOLE_0: 3;

              yf = (f . q) by A11, FUNCT_1: 1;

              hence thesis by A2, A10, A12, A14;

            end;

            ( dom f) = the carrier of S by FUNCT_2:def 1;

            then [x, (f . p)] in f by A3, FUNCT_1:def 2;

            then x in (f " W) by A6, RELAT_1:def 14;

            hence x in Q by A9, XBOOLE_0:def 4;

          end;

          given Q be Subset of S such that Q is open and

           A15: Q c= X & x in Q;

          thus thesis by A15;

        end;

        hence thesis by TOPS_1: 25;

      end;

      then

       A16: A is open;

      let X be Subset of S such that

       A17: X = { p where p be Point of S : (f . p) = (g . p) };

      (X ` ) = A

      proof

        hereby

          let x be object;

          assume

           A18: x in (X ` );

          then not x in X by XBOOLE_0:def 5;

          then (f . x) <> (g . x) by A17, A18;

          hence x in A by A18;

        end;

        let x be object;

        assume x in A;

        then

        consider p be Point of S such that

         A19: x = p and

         A20: (f . p) <> (g . p);

        now

          assume p in { t where t be Point of S : (f . t) = (g . t) };

          then ex t be Point of S st p = t & (f . t) = (g . t);

          hence contradiction by A20;

        end;

        hence thesis by A17, A19, XBOOLE_0:def 5;

      end;

      hence thesis by A16;

    end;

    theorem :: YELLOW12:46

    T is Hausdorff iff for A be Subset of [:T, T:] st A = ( id the carrier of T) holds A is closed

    proof

      reconsider f = ( pr1 (the carrier of T,the carrier of T)), g = ( pr2 (the carrier of T,the carrier of T)) as continuous Function of [:T, T:], T by Th39, Th40;

      reconsider A = ( id the carrier of T) as Subset of [:T, T:] by BORSUK_1:def 2;

      hereby

        assume

         A1: T is Hausdorff;

        let A be Subset of [:T, T:];

        assume A = ( id the carrier of T);

        then A = { p where p be Point of [:T, T:] : (f . p) = (g . p) } by Th37;

        hence A is closed by A1, Th45;

      end;

      assume for A be Subset of [:T, T:] st A = ( id the carrier of T) holds A is closed;

      then ( [#] [:T, T:]) = [:( [#] T), ( [#] T):] & A is closed by BORSUK_1:def 2;

      then ( [:( [#] T), ( [#] T):] \ A) is open;

      then

      consider SF be Subset-Family of [:T, T:] such that

       A2: ( [:( [#] T), ( [#] T):] \ A) = ( union SF) and

       A3: for e be set st e in SF holds ex X1,Y1 be Subset of T st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

      let p,q be Point of T;

      assume not p = q;

      then the carrier of [:T, T:] = [:the carrier of T, the carrier of T:] & not [p, q] in ( id ( [#] T)) by BORSUK_1:def 2, RELAT_1:def 10;

      then [p, q] in ( [:( [#] T), ( [#] T):] \ A) by XBOOLE_0:def 5;

      then

      consider XY be set such that

       A4: [p, q] in XY and

       A5: XY in SF by A2, TARSKI:def 4;

      consider X1,Y1 be Subset of T such that

       A6: XY = [:X1, Y1:] and

       A7: X1 is open & Y1 is open by A3, A5;

      take X1, Y1;

      thus X1 is open & Y1 is open by A7;

      thus p in X1 & q in Y1 by A4, A6, ZFMISC_1: 87;

      assume (X1 /\ Y1) <> {} ;

      then

      consider w be object such that

       A8: w in (X1 /\ Y1) by XBOOLE_0:def 1;

      w in X1 & w in Y1 by A8, XBOOLE_0:def 4;

      then [w, w] in XY by A6, ZFMISC_1: 87;

      then [w, w] in ( union SF) by A5, TARSKI:def 4;

      then not [w, w] in A by A2, XBOOLE_0:def 5;

      hence contradiction by A8, RELAT_1:def 10;

    end;

    registration

      let S,T be TopStruct;

      cluster strict for Refinement of S, T;

      existence

      proof

        set R = the Refinement of S, T;

        set R1 = the TopStruct of R;

        (the topology of S \/ the topology of T) is prebasis of R by YELLOW_9:def 6;

        then the carrier of R1 = (the carrier of S \/ the carrier of T) & (the topology of S \/ the topology of T) is prebasis of R1 by Th33, YELLOW_9:def 6;

        then

        reconsider R1 as Refinement of S, T by YELLOW_9:def 6;

        take R1;

        thus thesis;

      end;

    end

    registration

      let S be non empty TopStruct, T be TopStruct;

      cluster strict non empty for Refinement of S, T;

      existence

      proof

        set R = the strict Refinement of S, T;

        take R;

        thus thesis;

      end;

      cluster strict non empty for Refinement of T, S;

      existence

      proof

        set R = the strict Refinement of T, S;

        take R;

        thus thesis;

      end;

    end

    theorem :: YELLOW12:47

    for R,S,T be TopStruct holds R is Refinement of S, T iff the TopStruct of R is Refinement of S, T

    proof

      let R,S,T be TopStruct;

      hereby

        assume

         A1: R is Refinement of S, T;

        then

        reconsider R1 = R as TopSpace;

        (the topology of S \/ the topology of T) is prebasis of R by A1, YELLOW_9:def 6;

        then

         A2: (the topology of S \/ the topology of T) is prebasis of the TopStruct of R1 by Th33;

        the carrier of the TopStruct of R1 = (the carrier of S \/ the carrier of T) by A1, YELLOW_9:def 6;

        hence the TopStruct of R is Refinement of S, T by A2, YELLOW_9:def 6;

      end;

      assume

       A3: the TopStruct of R is Refinement of S, T;

      then

      reconsider R1 = R as TopSpace by TEX_2: 7;

      (the topology of S \/ the topology of T) is prebasis of the TopStruct of R by A3, YELLOW_9:def 6;

      then

       A4: (the topology of S \/ the topology of T) is prebasis of R1 by Th33;

      the carrier of R1 = (the carrier of S \/ the carrier of T) by A3, YELLOW_9:def 6;

      hence thesis by A4, YELLOW_9:def 6;

    end;

    reserve S1,S2,T1,T2 for non empty TopSpace,

R for Refinement of [:S1, T1:], [:S2, T2:],

R1 for Refinement of S1, S2,

R2 for Refinement of T1, T2;

    theorem :: YELLOW12:48

    

     Th48: the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies { ( [:U1, V1:] /\ [:U2, V2:]) where U1 be Subset of S1, U2 be Subset of S2, V1 be Subset of T1, V2 be Subset of T2 : U1 is open & U2 is open & V1 is open & V2 is open } is Basis of R

    proof

      assume

       A1: the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2;

      set Y = { ( [:U1, V1:] /\ [:U2, V2:]) where U1 be Subset of S1, U2 be Subset of S2, V1 be Subset of T1, V2 be Subset of T2 : U1 is open & U2 is open & V1 is open & V2 is open };

      

       A2: the carrier of [:S2, T2:] = [:the carrier of S2, the carrier of T2:] by BORSUK_1:def 2;

      

       A3: the carrier of [:S1, T1:] = [:the carrier of S1, the carrier of T1:] by BORSUK_1:def 2;

      then

      reconsider BST = ( INTERSECTION (the topology of [:S1, T1:],the topology of [:S2, T2:])) as Basis of R by A1, A2, YELLOW_9: 60;

      

       A4: the carrier of R = (the carrier of [:S1, T1:] \/ the carrier of [:S2, T2:]) by YELLOW_9:def 6

      .= ( [:the carrier of S1, the carrier of T1:] \/ [:the carrier of S2, the carrier of T2:]) by A3, BORSUK_1:def 2

      .= [:the carrier of S1, the carrier of T1:] by A1;

      Y c= ( bool the carrier of R)

      proof

        let c be object;

        assume c in Y;

        then ex U1 be Subset of S1, U2 be Subset of S2, V1 be Subset of T1, V2 be Subset of T2 st c = ( [:U1, V1:] /\ [:U2, V2:]) & U1 is open & U2 is open & V1 is open & V2 is open;

        hence thesis by A1, A2, A4;

      end;

      then

      reconsider C1 = Y as Subset-Family of R;

      reconsider C1 as Subset-Family of R;

      

       A5: the topology of [:S2, T2:] = { ( union A) where A be Subset-Family of [:S2, T2:] : A c= { [:X1, Y1:] where X1 be Subset of S2, Y1 be Subset of T2 : X1 in the topology of S2 & Y1 in the topology of T2 } } by BORSUK_1:def 2;

      

       A6: the topology of [:S1, T1:] = { ( union A) where A be Subset-Family of [:S1, T1:] : A c= { [:X1, Y1:] where X1 be Subset of S1, Y1 be Subset of T1 : X1 in the topology of S1 & Y1 in the topology of T1 } } by BORSUK_1:def 2;

      

       A7: for A be Subset of R st A is open holds for p be Point of R st p in A holds ex a be Subset of R st a in C1 & p in a & a c= A

      proof

        let A be Subset of R such that

         A8: A is open;

        let p be Point of R;

        assume p in A;

        then

        consider X be Subset of R such that

         A9: X in BST and

         A10: p in X and

         A11: X c= A by A8, YELLOW_9: 31;

        consider X1,X2 be set such that

         A12: X1 in the topology of [:S1, T1:] and

         A13: X2 in the topology of [:S2, T2:] and

         A14: X = (X1 /\ X2) by A9, SETFAM_1:def 5;

        consider F1 be Subset-Family of [:S1, T1:] such that

         A15: X1 = ( union F1) and

         A16: F1 c= { [:K1, L1:] where K1 be Subset of S1, L1 be Subset of T1 : K1 in the topology of S1 & L1 in the topology of T1 } by A6, A12;

        p in X1 by A10, A14, XBOOLE_0:def 4;

        then

        consider G1 be set such that

         A17: p in G1 and

         A18: G1 in F1 by A15, TARSKI:def 4;

        

         A19: G1 in { [:K1, L1:] where K1 be Subset of S1, L1 be Subset of T1 : K1 in the topology of S1 & L1 in the topology of T1 } by A16, A18;

        consider F2 be Subset-Family of [:S2, T2:] such that

         A20: X2 = ( union F2) and

         A21: F2 c= { [:K2, L2:] where K2 be Subset of S2, L2 be Subset of T2 : K2 in the topology of S2 & L2 in the topology of T2 } by A5, A13;

        p in X2 by A10, A14, XBOOLE_0:def 4;

        then

        consider G2 be set such that

         A22: p in G2 and

         A23: G2 in F2 by A20, TARSKI:def 4;

        G2 in { [:K2, L2:] where K2 be Subset of S2, L2 be Subset of T2 : K2 in the topology of S2 & L2 in the topology of T2 } by A21, A23;

        then

        consider K2 be Subset of S2, L2 be Subset of T2 such that

         A24: G2 = [:K2, L2:] and

         A25: K2 in the topology of S2 & L2 in the topology of T2;

        

         A26: [:K2, L2:] c= X2 by A20, A23, A24, ZFMISC_1: 74;

        

         A27: K2 is open & L2 is open by A25;

        consider K1 be Subset of S1, L1 be Subset of T1 such that

         A28: G1 = [:K1, L1:] and

         A29: K1 in the topology of S1 & L1 in the topology of T1 by A19;

        reconsider a = ( [:K1, L1:] /\ [:K2, L2:]) as Subset of R by A1, A4, BORSUK_1:def 2;

        take a;

        K1 is open & L1 is open by A29;

        hence a in C1 by A27;

        thus p in a by A17, A22, A28, A24, XBOOLE_0:def 4;

         [:K1, L1:] c= X1 by A15, A18, A28, ZFMISC_1: 74;

        then a c= X by A14, A26, XBOOLE_1: 27;

        hence thesis by A11;

      end;

      Y c= the topology of R

      proof

        let c be object;

        

         A30: BST c= the topology of R by TOPS_2: 64;

        assume c in Y;

        then

        consider U1 be Subset of S1, U2 be Subset of S2, V1 be Subset of T1, V2 be Subset of T2 such that

         A31: c = ( [:U1, V1:] /\ [:U2, V2:]) and

         A32: U1 is open and

         A33: U2 is open and

         A34: V1 is open and

         A35: V2 is open;

         [:U2, V2:] is open by A33, A35, BORSUK_1: 6;

        then

         A36: [:U2, V2:] in the topology of [:S2, T2:];

         [:U1, V1:] is open by A32, A34, BORSUK_1: 6;

        then [:U1, V1:] in the topology of [:S1, T1:];

        then c in BST by A31, A36, SETFAM_1:def 5;

        hence thesis by A30;

      end;

      hence thesis by A7, YELLOW_9: 32;

    end;

    theorem :: YELLOW12:49

    

     Th49: the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies the carrier of [:R1, R2:] = the carrier of R & the topology of [:R1, R2:] = the topology of R

    proof

      assume that

       A1: the carrier of S1 = the carrier of S2 and

       A2: the carrier of T1 = the carrier of T2;

      

       A3: the carrier of R1 = (the carrier of S1 \/ the carrier of S2) by YELLOW_9:def 6

      .= the carrier of S1 by A1;

      set C = { ( [:U1, V1:] /\ [:U2, V2:]) where U1 be Subset of S1, U2 be Subset of S2, V1 be Subset of T1, V2 be Subset of T2 : U1 is open & U2 is open & V1 is open & V2 is open };

      reconsider BT = ( INTERSECTION (the topology of T1,the topology of T2)) as Basis of R2 by A2, YELLOW_9: 60;

      reconsider BS = ( INTERSECTION (the topology of S1,the topology of S2)) as Basis of R1 by A1, YELLOW_9: 60;

      reconsider Bpr = { [:a, b:] where a be Subset of R1, b be Subset of R2 : a in BS & b in BT } as Basis of [:R1, R2:] by YELLOW_9: 40;

      

       A4: C = Bpr

      proof

        hereby

          let c be object;

          assume c in C;

          then

          consider U1 be Subset of S1, U2 be Subset of S2, V1 be Subset of T1, V2 be Subset of T2 such that

           A5: c = ( [:U1, V1:] /\ [:U2, V2:]) and

           A6: U1 is open & U2 is open and

           A7: V1 is open & V2 is open;

          U1 in the topology of S1 & U2 in the topology of S2 by A6;

          then

           A8: (U1 /\ U2) in BS by SETFAM_1:def 5;

          V1 in the topology of T1 & V2 in the topology of T2 by A7;

          then

           A9: (V1 /\ V2) in BT by SETFAM_1:def 5;

          c = [:(U1 /\ U2), (V1 /\ V2):] by A5, ZFMISC_1: 100;

          hence c in Bpr by A8, A9;

        end;

        let c be object;

        assume c in Bpr;

        then

        consider a be Subset of R1, b be Subset of R2 such that

         A10: c = [:a, b:] and

         A11: a in BS and

         A12: b in BT;

        consider a1,a2 be set such that

         A13: a1 in the topology of S1 and

         A14: a2 in the topology of S2 and

         A15: a = (a1 /\ a2) by A11, SETFAM_1:def 5;

        reconsider a2 as Subset of S2 by A14;

        reconsider a1 as Subset of S1 by A13;

        

         A16: a1 is open & a2 is open by A13, A14;

        consider b1,b2 be set such that

         A17: b1 in the topology of T1 and

         A18: b2 in the topology of T2 and

         A19: b = (b1 /\ b2) by A12, SETFAM_1:def 5;

        reconsider b2 as Subset of T2 by A18;

        reconsider b1 as Subset of T1 by A17;

        

         A20: b1 is open & b2 is open by A17, A18;

        c = ( [:a1, b1:] /\ [:a2, b2:]) by A10, A15, A19, ZFMISC_1: 100;

        hence thesis by A16, A20;

      end;

      

       A21: the carrier of R2 = (the carrier of T1 \/ the carrier of T2) by YELLOW_9:def 6

      .= the carrier of T1 by A2;

      

       A22: the carrier of [:S1, T1:] = [:the carrier of S1, the carrier of T1:] by BORSUK_1:def 2;

      the carrier of R = (the carrier of [:S1, T1:] \/ the carrier of [:S2, T2:]) by YELLOW_9:def 6

      .= ( [:the carrier of S1, the carrier of T1:] \/ [:the carrier of S2, the carrier of T2:]) by A22, BORSUK_1:def 2

      .= [:the carrier of S1, the carrier of T1:] by A1, A2;

      hence

       A23: the carrier of [:R1, R2:] = the carrier of R by A3, A21, BORSUK_1:def 2;

      C is Basis of R by A1, A2, Th48;

      hence thesis by A23, A4, YELLOW_9: 25;

    end;

    theorem :: YELLOW12:50

    the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies [:R1, R2:] is Refinement of [:S1, T1:], [:S2, T2:]

    proof

      set R = the strict Refinement of [:S1, T1:], [:S2, T2:];

      assume

       A1: the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2;

      then the carrier of [:R1, R2:] = the carrier of R by Th49;

      hence thesis by A1, Th49;

    end;