waybel29.miz



    begin

    theorem :: WAYBEL29:1

    

     Th1: for X,Y be non empty set, Z be non empty RelStr holds for S be non empty SubRelStr of (Z |^ [:X, Y:]) holds for T be non empty SubRelStr of ((Z |^ Y) |^ X) holds for f be Function of S, T st f is currying one-to-one onto holds (f " ) is uncurrying

    proof

      let X,Y be non empty set, Z be non empty RelStr;

      let S be non empty SubRelStr of (Z |^ [:X, Y:]);

      let T be non empty SubRelStr of ((Z |^ Y) |^ X);

      let f be Function of S, T;

      assume

       A1: f is currying one-to-one onto;

      then

       A2: ( rng f) = the carrier of T by FUNCT_2:def 3;

      

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

      

       A4: ( Funcs (X,the carrier of (Z |^ Y))) = the carrier of ((Z |^ Y) |^ X) & ( Funcs (Y,the carrier of Z)) = the carrier of (Z |^ Y) by YELLOW_1: 28;

      hereby

        let x be set;

        assume x in ( dom (f " ));

        then x is Element of ((Z |^ Y) |^ X) by YELLOW_0: 58;

        then x is Function of X, ( Funcs (Y,the carrier of Z)) by A4, FUNCT_2: 66;

        hence x is Function-yielding Function;

      end;

      let g be Function;

      assume g in ( dom (f " ));

      then

      consider h be object such that

       A5: h in ( dom f) and

       A6: g = (f . h) by A2, FUNCT_1:def 3;

      reconsider h as Function by A5;

      ( Funcs ( [:X, Y:],the carrier of Z)) = the carrier of (Z |^ [:X, Y:]) & h is Element of (Z |^ [:X, Y:]) by A5, YELLOW_0: 58, YELLOW_1: 28;

      then h is Function of [:X, Y:], the carrier of Z by FUNCT_2: 66;

      then

       A7: ( dom h) = [:X, Y:] by FUNCT_2:def 1;

      g = ( curry h) by A1, A5, A6;

      then ( uncurry g) = h by A7, FUNCT_5: 49;

      hence thesis by A1, A3, A5, A6, FUNCT_1: 32;

    end;

    theorem :: WAYBEL29:2

    

     Th2: for X,Y be non empty set, Z be non empty RelStr holds for S be non empty SubRelStr of (Z |^ [:X, Y:]) holds for T be non empty SubRelStr of ((Z |^ Y) |^ X) holds for f be Function of T, S st f is uncurrying one-to-one onto holds (f " ) is currying

    proof

      let X,Y be non empty set, Z be non empty RelStr;

      let S be non empty SubRelStr of (Z |^ [:X, Y:]);

      let T be non empty SubRelStr of ((Z |^ Y) |^ X);

      let f be Function of T, S;

      

       A1: ( Funcs (X,the carrier of (Z |^ Y))) = the carrier of ((Z |^ Y) |^ X) & ( Funcs (Y,the carrier of Z)) = the carrier of (Z |^ Y) by YELLOW_1: 28;

      assume

       A2: f is uncurrying one-to-one onto;

      then

       A3: ( rng f) = the carrier of S by FUNCT_2:def 3;

      

       A4: (f " ) = (f qua Function " ) by A2, TOPS_2:def 4;

      

       A5: ( Funcs ( [:X, Y:],the carrier of Z)) = the carrier of (Z |^ [:X, Y:]) by YELLOW_1: 28;

      hereby

        let x be set;

        assume x in ( dom (f " ));

        then x is Element of (Z |^ [:X, Y:]) by YELLOW_0: 58;

        then

        reconsider g = x as Function of [:X, Y:], the carrier of Z by A5, FUNCT_2: 66;

        ( dom g) = ( proj1 g);

        hence x is Function & ( proj1 x) is Relation;

      end;

      let g be Function;

      assume g in ( dom (f " ));

      then

      consider h be object such that

       A6: h in ( dom f) and

       A7: g = (f . h) by A3, FUNCT_1:def 3;

      reconsider h as Function by A6;

      h is Element of ((Z |^ Y) |^ X) by A6, YELLOW_0: 58;

      then h is Function of X, ( Funcs (Y,the carrier of Z)) by A1, FUNCT_2: 66;

      then

       A8: ( rng h) c= ( Funcs (Y,the carrier of Z)) by RELAT_1:def 19;

      g = ( uncurry h) by A2, A6, A7;

      then ( curry g) = h by A8, FUNCT_5: 48;

      hence thesis by A2, A4, A6, A7, FUNCT_1: 32;

    end;

    theorem :: WAYBEL29:3

    for X,Y be non empty set, Z be non empty Poset holds for S be non empty full SubRelStr of (Z |^ [:X, Y:]) holds for T be non empty full SubRelStr of ((Z |^ Y) |^ X) holds for f be Function of S, T st f is currying one-to-one onto holds f is isomorphic

    proof

      let X,Y be non empty set, Z be non empty Poset;

      let S be non empty full SubRelStr of (Z |^ [:X, Y:]);

      let T be non empty full SubRelStr of ((Z |^ Y) |^ X);

      let f be Function of S, T;

      assume

       A1: f is currying one-to-one onto;

      then

       A2: (f * (f " )) = ( id T) & ((f " ) * f) = ( id S) by GRCAT_1: 41;

      f is monotone & (f " ) is monotone by A1, Th1, WAYBEL27: 20, WAYBEL27: 21;

      hence thesis by A2, YELLOW16: 15;

    end;

    theorem :: WAYBEL29:4

    for X,Y be non empty set, Z be non empty Poset holds for T be non empty full SubRelStr of (Z |^ [:X, Y:]) holds for S be non empty full SubRelStr of ((Z |^ Y) |^ X) holds for f be Function of S, T st f is uncurrying one-to-one onto holds f is isomorphic

    proof

      let X,Y be non empty set, Z be non empty Poset;

      let T be non empty full SubRelStr of (Z |^ [:X, Y:]);

      let S be non empty full SubRelStr of ((Z |^ Y) |^ X);

      let f be Function of S, T;

      assume

       A1: f is uncurrying one-to-one onto;

      then

       A2: (f * (f " )) = ( id T) & ((f " ) * f) = ( id S) by GRCAT_1: 41;

      f is monotone & (f " ) is monotone by A1, Th2, WAYBEL27: 20, WAYBEL27: 21;

      hence thesis by A2, YELLOW16: 15;

    end;

    theorem :: WAYBEL29:5

    

     Th5: for S1,S2,T1,T2 be RelStr st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2 holds for f be Function of S1, T1 st f is isomorphic holds for g be Function of S2, T2 st g = f holds g is isomorphic

    proof

      let S1,S2,T1,T2 be RelStr such that

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

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

      let f be Function of S1, T1 such that

       A3: f is isomorphic;

      let g be Function of S2, T2 such that

       A4: g = f;

      per cases ;

        suppose

         A5: S1 is empty;

        then T1 is empty by A3, WAYBEL_0:def 38;

        then

         A6: T2 is empty by A2;

        S2 is empty by A1, A5;

        hence thesis by A6, WAYBEL_0:def 38;

      end;

        suppose S1 is non empty;

        then

        reconsider S1, T1 as non empty RelStr by A3, WAYBEL_0:def 38;

        reconsider f as Function of S1, T1;

        the carrier of S1 <> {} & the carrier of T1 <> {} ;

        then

        reconsider S2, T2 as non empty RelStr by A1, A2;

        reconsider g as Function of S2, T2;

         A7:

        now

          let x,y be Element of S2;

          reconsider a = x, b = y as Element of S1 by A1;

          

           A8: x <= y iff a <= b by A1, YELLOW_0: 1;

          (g . x) <= (g . y) iff (f . a) <= (f . b) by A2, A4, YELLOW_0: 1;

          hence x <= y iff (g . x) <= (g . y) by A3, A8, WAYBEL_0: 66;

        end;

        ( rng f) = the carrier of T1 by A3, WAYBEL_0: 66;

        hence thesis by A2, A3, A4, A7, WAYBEL_0: 66;

      end;

    end;

    theorem :: WAYBEL29:6

    

     Th6: for R,S,T be RelStr holds for f be Function of R, S st f is isomorphic holds for g be Function of S, T st g is isomorphic holds for h be Function of R, T st h = (g * f) holds h is isomorphic

    proof

      let L1,L2,L3 be RelStr;

      let f1 be Function of L1, L2 such that

       A1: f1 is isomorphic;

      let f2 be Function of L2, L3 such that

       A2: f2 is isomorphic;

      let h be Function of L1, L3 such that

       A3: h = (f2 * f1);

      per cases ;

        suppose L1 is non empty & L2 is non empty & L3 is non empty;

        then

        reconsider L1, L2, L3 as non empty RelStr;

        reconsider f1 as Function of L1, L2;

        reconsider f2 as Function of L2, L3;

        consider g1 be Function of L2, L1 such that

         A4: g1 = (f1 qua Function " ) & g1 is monotone by A1, WAYBEL_0:def 38;

        consider g2 be Function of L3, L2 such that

         A5: g2 = (f2 qua Function " ) & g2 is monotone by A2, WAYBEL_0:def 38;

        

         A6: (f2 * f1) is monotone by A1, A2, YELLOW_2: 12;

        (g1 * g2) is monotone & (g1 * g2) = ((f2 * f1) qua Function " ) by A1, A2, A4, A5, FUNCT_1: 44, YELLOW_2: 12;

        hence thesis by A1, A2, A3, A6, WAYBEL_0:def 38;

      end;

        suppose

         A7: L1 is empty;

        then L2 is empty by A1, WAYBEL_0:def 38;

        then L3 is empty by A2, WAYBEL_0:def 38;

        hence thesis by A7, WAYBEL_0:def 38;

      end;

        suppose L2 is empty;

        then L1 is empty & L3 is empty by A1, A2, WAYBEL_0:def 38;

        hence thesis by WAYBEL_0:def 38;

      end;

        suppose

         A8: L3 is empty;

        then L2 is empty by A2, WAYBEL_0:def 38;

        then L1 is empty by A1, WAYBEL_0:def 38;

        hence thesis by A8, WAYBEL_0:def 38;

      end;

    end;

    theorem :: WAYBEL29:7

    

     Th7: for X,Y,X1,Y1 be TopSpace st the TopStruct of X = the TopStruct of X1 & the TopStruct of Y = the TopStruct of Y1 holds [:X, Y:] = [:X1, Y1:]

    proof

      let X,Y,X1,Y1 be TopSpace;

      assume

       A1: the TopStruct of X = the TopStruct of X1 & the TopStruct of Y = the TopStruct of Y1;

      set U2 = { ( union A) where A be Subset-Family of [:X1, Y1:] : A c= { [:X2, Y2:] where X2 be Subset of X1, Y2 be Subset of Y1 : X2 in the topology of X1 & Y2 in the topology of Y1 } };

      

       A2: the carrier of [:X, Y:] = [:the carrier of X, the carrier of Y:] by BORSUK_1:def 2

      .= the carrier of [:X1, Y1:] by A1, BORSUK_1:def 2;

      

      then the topology of [:X, Y:] = U2 by A1, BORSUK_1:def 2

      .= the topology of [:X1, Y1:] by BORSUK_1:def 2;

      hence thesis by A2;

    end;

    theorem :: WAYBEL29:8

    

     Th8: for X be non empty TopSpace holds for L be Scott up-complete non empty TopPoset holds for F be non empty directed Subset of ( ContMaps (X,L)) holds ( "\/" (F,(L |^ the carrier of X))) is continuous Function of X, L

    proof

      let X be non empty TopSpace;

      let L be Scott up-complete non empty TopPoset;

      let F be non empty directed Subset of ( ContMaps (X,L));

      set sF = ( "\/" (F,(L |^ the carrier of X)));

      ( Funcs (the carrier of X,the carrier of L)) = the carrier of (L |^ the carrier of X) by YELLOW_1: 28;

      then

      reconsider sF as Function of X, L by FUNCT_2: 66;

      ( ContMaps (X,L)) is full SubRelStr of (L |^ the carrier of X) by WAYBEL24:def 3;

      then

      reconsider aF = F as non empty directed Subset of (L |^ the carrier of X) by YELLOW_2: 7;

       A1:

      now

        let A be Subset of L;

        assume

         A2: A is open;

        now

          let x be set;

          hereby

            assume

             A3: x in (sF " A);

            then

             A4: (sF . x) in A by FUNCT_1:def 7;

            reconsider y = x as Element of X by A3;

            

             A5: (the carrier of X -POS_prod (the carrier of X => L)) = (L |^ the carrier of X) by YELLOW_1:def 5;

            

             A6: ((the carrier of X => L) . y) = L;

            then

             A7: ( pi (aF,y)) is directed non empty by A5, YELLOW16: 35;

            

             A8: ex_sup_of (aF,(L |^ the carrier of X)) by WAYBEL_0: 75;

            then (( sup aF) . y) = ( sup ( pi (aF,y))) by A6, A5, YELLOW16: 33;

            then ( pi (aF,y)) meets A by A2, A4, A7, WAYBEL11:def 1;

            then

            consider a be object such that

             A9: a in ( pi (aF,y)) and

             A10: a in A by XBOOLE_0: 3;

            consider f be Function such that

             A11: f in aF and

             A12: a = (f . y) by A9, CARD_3:def 6;

            reconsider f as continuous Function of X, L by A11, WAYBEL24: 21;

            take Q = (f " A);

            ( [#] L) <> {} ;

            hence Q is open by A2, TOPS_2: 43;

            

             A13: ( dom sF) = the carrier of X by FUNCT_2:def 1;

            thus Q c= (sF " A)

            proof

              let b be object;

              assume

               A14: b in Q;

              then

               A15: (f . b) in A by FUNCT_1:def 7;

              reconsider b as Element of X by A14;

              

               A16: ((the carrier of X => L) . b) = L;

              then ( pi (aF,b)) is directed non empty by A5, YELLOW16: 35;

              then

               A17: ex_sup_of (( pi (aF,b)),L) by WAYBEL_0: 75;

              (sF . b) = ( sup ( pi (aF,b))) by A8, A5, A16, YELLOW16: 33;

              then

               A18: (sF . b) is_>=_than ( pi (aF,b)) by A17, YELLOW_0: 30;

              (f . b) in ( pi (aF,b)) by A11, CARD_3:def 6;

              then (f . b) <= (sF . b) by A18;

              then (sF . b) in A by A2, A15, WAYBEL_0:def 20;

              hence thesis by A13, FUNCT_1:def 7;

            end;

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

            hence x in Q by A10, A12, FUNCT_1:def 7;

          end;

          thus (ex Q be Subset of X st Q is open & Q c= (sF " A) & x in Q) implies x in (sF " A);

        end;

        hence (sF " A) is open by TOPS_1: 25;

      end;

      ( [#] L) <> {} ;

      hence thesis by A1, TOPS_2: 43;

    end;

    theorem :: WAYBEL29:9

    

     Th9: for X be non empty TopSpace holds for L be Scott up-complete non empty TopPoset holds ( ContMaps (X,L)) is directed-sups-inheriting SubRelStr of (L |^ the carrier of X)

    proof

      let X be non empty TopSpace;

      let L be Scott up-complete non empty TopPoset;

      reconsider XL = ( ContMaps (X,L)) as non empty full SubRelStr of (L |^ the carrier of X) by WAYBEL24:def 3;

      XL is directed-sups-inheriting

      proof

        let A be directed Subset of XL;

        assume that

         A1: A <> {} and ex_sup_of (A,(L |^ the carrier of X));

        reconsider A as directed non empty Subset of XL by A1;

        ( "\/" (A,(L |^ the carrier of X))) is continuous Function of X, L by Th8;

        hence thesis by WAYBEL24:def 3;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL29:10

    

     Th10: for S1,S2 be TopStruct st the TopStruct of S1 = the TopStruct of S2 holds for T1,T2 be non empty TopRelStr st the TopRelStr of T1 = the TopRelStr of T2 holds ( ContMaps (S1,T1)) = ( ContMaps (S2,T2))

    proof

      let S1,S2 be TopStruct;

      assume

       A1: the TopStruct of S1 = the TopStruct of S2;

      let T1,T2 be non empty TopRelStr;

      assume

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

      then the RelStr of T1 = the RelStr of T2;

      then (T1 |^ the carrier of S1) = (T2 |^ the carrier of S2) by A1, WAYBEL27: 15;

      then

      reconsider C2 = ( ContMaps (S2,T2)) as full SubRelStr of (T1 |^ the carrier of S1) by WAYBEL24:def 3;

      reconsider C1 = ( ContMaps (S1,T1)) as full SubRelStr of (T1 |^ the carrier of S1) by WAYBEL24:def 3;

      the carrier of ( ContMaps (S1,T1)) = the carrier of ( ContMaps (S2,T2))

      proof

        thus the carrier of ( ContMaps (S1,T1)) c= the carrier of ( ContMaps (S2,T2))

        proof

          let x be object;

          assume x in the carrier of ( ContMaps (S1,T1));

          then

          consider f be Function of S1, T1 such that

           A3: x = f and

           A4: f is continuous by WAYBEL24:def 3;

          reconsider f2 = f as Function of S2, T2 by A1, A2;

          f2 is continuous

          proof

            let P2 be Subset of T2;

            reconsider P1 = P2 as Subset of T1 by A2;

            assume P2 is closed;

            then (( [#] T2) \ P2) is open;

            then (( [#] T2) \ P2) in the topology of T2;

            then (( [#] T1) \ P1) is open by A2;

            then P1 is closed;

            then (f " P1) is closed by A4;

            then (( [#] S1) \ (f " P1)) is open;

            then (( [#] S1) \ (f2 " P2)) in the topology of S2 by A1;

            then (( [#] S2) \ (f2 " P2)) is open by A1;

            hence thesis;

          end;

          hence thesis by A3, WAYBEL24:def 3;

        end;

        let x be object;

        assume x in the carrier of ( ContMaps (S2,T2));

        then

        consider f be Function of S2, T2 such that

         A5: x = f and

         A6: f is continuous by WAYBEL24:def 3;

        reconsider f1 = f as Function of S1, T1 by A1, A2;

        f1 is continuous

        proof

          let P1 be Subset of T1;

          reconsider P2 = P1 as Subset of T2 by A2;

          assume P1 is closed;

          then (( [#] T1) \ P1) is open;

          then (( [#] T1) \ P2) in the topology of T2 by A2;

          then (( [#] T2) \ P2) is open by A2;

          then P2 is closed;

          then (f " P2) is closed by A6;

          then (( [#] S2) \ (f " P2)) is open;

          then (( [#] S2) \ (f1 " P1)) in the topology of S1 by A1;

          then (( [#] S1) \ (f1 " P1)) is open by A1;

          hence thesis;

        end;

        hence thesis by A5, WAYBEL24:def 3;

      end;

      then the RelStr of C1 = the RelStr of C2 by YELLOW_0: 57;

      hence thesis;

    end;

    registration

      cluster Scott -> injective T_0 for complete continuous TopLattice;

      coherence

      proof

        let T be complete continuous TopLattice;

        assume T is Scott;

        then T is Scott TopAugmentation of T by YELLOW_9: 44;

        hence thesis;

      end;

    end

    registration

      cluster Scott continuous complete for TopLattice;

      existence

      proof

        set L = the continuous complete LATTICE;

        set T = the Scott TopAugmentation of L;

        take T;

        thus thesis;

      end;

    end

    registration

      let X be non empty TopSpace;

      let L be Scott up-complete non empty TopPoset;

      cluster ( ContMaps (X,L)) -> up-complete;

      coherence

      proof

        ( ContMaps (X,L)) is full directed-sups-inheriting SubRelStr of (L |^ the carrier of X) by Th9, WAYBEL24:def 3;

        hence thesis by YELLOW16: 5;

      end;

    end

    theorem :: WAYBEL29:11

    

     Th11: for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is up-complete holds (I -POS_prod J) is up-complete

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is up-complete;

      set L = (I -POS_prod J);

      now

        let A be non empty directed Subset of L;

        now

          let x be Element of I;

          (J . x) is up-complete non empty Poset & ( pi (A,x)) is directed non empty by A1, YELLOW16: 35;

          hence ex_sup_of (( pi (A,x)),(J . x)) by WAYBEL_0: 75;

        end;

        hence ex_sup_of (A,L) by YELLOW16: 31;

      end;

      hence thesis by WAYBEL_0: 75;

    end;

    theorem :: WAYBEL29:12

    for I be non empty set holds for J be Poset-yielding non-Empty ManySortedSet of I st for i be Element of I holds (J . i) is up-complete lower-bounded holds for x,y be Element of ( product J) holds x << y iff (for i be Element of I holds (x . i) << (y . i)) & ex K be finite Subset of I st for i be Element of I st not i in K holds (x . i) = ( Bottom (J . i))

    proof

      let I be non empty set;

      let J be Poset-yielding non-Empty ManySortedSet of I;

      set L = ( product J);

      assume

       A1: for i be Element of I holds (J . i) is up-complete lower-bounded;

      then

      reconsider L9 = L as up-complete non empty Poset by Th11;

      let x,y be Element of L;

      hereby

        assume

         A2: x << y;

        hereby

          let i be Element of I;

          thus (x . i) << (y . i)

          proof

            let Di be non empty directed Subset of (J . i) such that

             A3: (y . i) <= ( sup Di);

            set di = the Element of Di;

            set D = { (y +* (i,z)) where z be Element of (J . i) : z in Di };

            reconsider di as Element of (J . i);

            

             A4: ( dom y) = I by WAYBEL_3: 27;

            D c= the carrier of L

            proof

              let a be object;

              assume a in D;

              then

              consider z be Element of (J . i) such that

               A5: a = (y +* (i,z)) and z in Di;

               A6:

              now

                let j be Element of I;

                i = j or i <> j;

                then ((y +* (i,z)) . j) = z & i = j or ((y +* (i,z)) . j) = (y . j) by A4, FUNCT_7: 31, FUNCT_7: 32;

                hence ((y +* (i,z)) . j) is Element of (J . j);

              end;

              ( dom (y +* (i,z))) = I by A4, FUNCT_7: 30;

              then a is Element of L by A5, A6, WAYBEL_3: 27;

              hence thesis;

            end;

            then

            reconsider D as Subset of L;

            

             A7: (y +* (i,di)) in D;

            then

            reconsider D as non empty Subset of L;

            D is directed

            proof

              let z1,z2 be Element of L;

              assume z1 in D;

              then

              consider a1 be Element of (J . i) such that

               A8: z1 = (y +* (i,a1)) and

               A9: a1 in Di;

              assume z2 in D;

              then

              consider a2 be Element of (J . i) such that

               A10: z2 = (y +* (i,a2)) and

               A11: a2 in Di;

              consider a be Element of (J . i) such that

               A12: a in Di and

               A13: a >= a1 and

               A14: a >= a2 by A9, A11, WAYBEL_0:def 1;

              (y +* (i,a)) in D by A12;

              then

              reconsider z = (y +* (i,a)) as Element of L;

              take z;

              thus z in D by A12;

              

               A15: ( dom y) = I by WAYBEL_3: 27;

              now

                let j be Element of I;

                i = j or i <> j;

                then (z . j) = a & (z1 . j) = a1 & i = j or (z . j) = (y . j) & (z1 . j) = (y . j) by A8, A15, FUNCT_7: 31, FUNCT_7: 32;

                hence (z . j) >= (z1 . j) by A13, YELLOW_0:def 1;

              end;

              hence z >= z1 by WAYBEL_3: 28;

              now

                let j be Element of I;

                i = j or i <> j;

                then (z . j) = a & (z2 . j) = a2 & i = j or (z . j) = (y . j) & (z2 . j) = (y . j) by A10, A15, FUNCT_7: 31, FUNCT_7: 32;

                hence (z . j) >= (z2 . j) by A14, YELLOW_0:def 1;

              end;

              hence thesis by WAYBEL_3: 28;

            end;

            then

            reconsider D as non empty directed Subset of L;

            

             A16: ( dom y) = I by WAYBEL_3: 27;

            now

              

               A17: Di c= ( pi (D,i))

              proof

                let a be object;

                assume

                 A18: a in Di;

                then

                reconsider a as Element of (J . i);

                (y +* (i,a)) in D by A18;

                then ((y +* (i,a)) . i) in ( pi (D,i)) by CARD_3:def 6;

                hence thesis by A16, FUNCT_7: 31;

              end;

              let j be Element of I;

              

               A19: (J . i) is up-complete non empty Poset & (J . j) is up-complete non empty Poset by A1;

              ( pi (D,i)) is non empty directed by YELLOW16: 35;

              then

               A20: ex_sup_of (( pi (D,i)),(J . i)) by A19, WAYBEL_0: 75;

               ex_sup_of (Di,(J . i)) by A19, WAYBEL_0: 75;

              then

               A21: ( sup Di) <= ( sup ( pi (D,i))) by A20, A17, YELLOW_0: 34;

               ex_sup_of (D,L9) by WAYBEL_0: 75;

              then

               A22: (( sup D) . j) = ( sup ( pi (D,j))) by YELLOW16: 33;

               A23:

              now

                assume j <> i;

                then ((y +* (i,di)) . j) = (y . j) by FUNCT_7: 32;

                hence (y . j) in ( pi (D,j)) by A7, CARD_3:def 6;

              end;

              ( pi (D,j)) is non empty directed by YELLOW16: 35;

              then ex_sup_of (( pi (D,j)),(J . j)) by A19, WAYBEL_0: 75;

              then (( sup D) . j) is_>=_than ( pi (D,j)) by A22, YELLOW_0: 30;

              hence (( sup D) . j) >= (y . j) by A3, A21, A22, A23, YELLOW_0:def 2;

            end;

            then ( sup D) >= y by WAYBEL_3: 28;

            then

            consider d be Element of L such that

             A24: d in D and

             A25: d >= x by A2;

            consider z be Element of (J . i) such that

             A26: d = (y +* (i,z)) and

             A27: z in Di by A24;

            take z;

            (d . i) = z by A4, A26, FUNCT_7: 31;

            hence thesis by A25, A27, WAYBEL_3: 28;

          end;

        end;

        set K = { i where i be Element of I : (x . i) <> ( Bottom (J . i)) };

        K c= I

        proof

          let a be object;

          assume a in K;

          then ex i be Element of I st a = i & (x . i) <> ( Bottom (J . i));

          hence thesis;

        end;

        then

        reconsider K as Subset of I;

        deffunc F( Element of I) = ( Bottom (J . $1));

        consider f be ManySortedSet of I such that

         A28: for i be Element of I holds (f . i) = F(i) from PBOOLE:sch 5;

         A29:

        now

          let i be Element of I;

          (f . i) = ( Bottom (J . i)) by A28;

          hence (f . i) is Element of (J . i);

        end;

        

         A30: ( dom f) = I by PARTFUN1:def 2;

        then

        reconsider f as Element of ( product J) by A29, WAYBEL_3: 27;

        set X = the set of all (f +* (y | a)) where a be finite Subset of I;

        X c= the carrier of L

        proof

          let a be object;

          assume a in X;

          then

          consider b be finite Subset of I such that

           A31: a = (f +* (y | b));

          ( dom y) = I by WAYBEL_3: 27;

          then

           A32: ( dom (y | b)) = b by RELAT_1: 62;

           A33:

          now

            let i be Element of I;

            ((f +* (y | b)) . i) = (f . i) or ((f +* (y | b)) . i) = ((y | b) . i) & ((y | b) . i) = (y . i) by A32, FUNCT_1: 47, FUNCT_4: 11, FUNCT_4: 13;

            hence ((f +* (y | b)) . i) is Element of (J . i);

          end;

          I = (I \/ ( dom (y | b))) by A32, XBOOLE_1: 12

          .= ( dom (f +* (y | b))) by A30, FUNCT_4:def 1;

          then a is Element of L by A31, A33, WAYBEL_3: 27;

          hence thesis;

        end;

        then

        reconsider X as Subset of L;

        (f +* (y | ( {} I) qua finite Subset of I)) in X;

        then

        reconsider X as non empty Subset of L;

        X is directed

        proof

          let z1,z2 be Element of L;

          assume z1 in X;

          then

          consider a1 be finite Subset of I such that

           A34: z1 = (f +* (y | a1));

          assume z2 in X;

          then

          consider a2 be finite Subset of I such that

           A35: z2 = (f +* (y | a2));

          reconsider a = (a1 \/ a2) as finite Subset of I;

          (f +* (y | a)) in X;

          then

          reconsider z = (f +* (y | a)) as Element of L;

          take z;

          thus z in X;

          

           A36: ( dom y) = I by WAYBEL_3: 27;

          then

           A37: ( dom (y | a)) = a by RELAT_1: 62;

          

           A38: ( dom (y | a1)) = a1 by A36, RELAT_1: 62;

          now

            let i be Element of I;

            

             A39: (f . i) = ( Bottom (J . i)) by A28;

            (J . i) is up-complete lower-bounded non empty Poset by A1;

            then

             A40: ( Bottom (J . i)) <= (y . i) by YELLOW_0: 44;

            per cases by XBOOLE_0:def 3;

              suppose

               A41: not i in a1 & i in a;

              then (z . i) = ((y | a) . i) & ((y | a) . i) = (y . i) by A37, FUNCT_1: 47, FUNCT_4: 13;

              hence (z . i) >= (z1 . i) by A34, A38, A40, A39, A41, FUNCT_4: 11;

            end;

              suppose not i in a & not i in a1;

              then (z . i) = (f . i) & (z1 . i) = (f . i) by A34, A37, A38, FUNCT_4: 11;

              hence (z . i) >= (z1 . i) by YELLOW_0:def 1;

            end;

              suppose

               A42: i in a1 & i in a;

              then

               A43: (z . i) = ((y | a) . i) & ((y | a) . i) = (y . i) by A37, FUNCT_1: 47, FUNCT_4: 13;

              (z1 . i) = ((y | a1) . i) & ((y | a1) . i) = (y . i) by A34, A38, A42, FUNCT_1: 47, FUNCT_4: 13;

              hence (z . i) >= (z1 . i) by A43, YELLOW_0:def 1;

            end;

          end;

          hence z >= z1 by WAYBEL_3: 28;

          

           A44: ( dom (y | a2)) = a2 by A36, RELAT_1: 62;

          now

            let i be Element of I;

            

             A45: (f . i) = ( Bottom (J . i)) by A28;

            (J . i) is up-complete lower-bounded non empty Poset by A1;

            then

             A46: ( Bottom (J . i)) <= (y . i) by YELLOW_0: 44;

            per cases by XBOOLE_0:def 3;

              suppose

               A47: not i in a2 & i in a;

              then (z . i) = ((y | a) . i) & ((y | a) . i) = (y . i) by A37, FUNCT_1: 47, FUNCT_4: 13;

              hence (z . i) >= (z2 . i) by A35, A44, A46, A45, A47, FUNCT_4: 11;

            end;

              suppose not i in a & not i in a2;

              then (z . i) = (f . i) & (z2 . i) = (f . i) by A35, A37, A44, FUNCT_4: 11;

              hence (z . i) >= (z2 . i) by YELLOW_0:def 1;

            end;

              suppose

               A48: i in a2 & i in a;

              then

               A49: (z . i) = ((y | a) . i) & ((y | a) . i) = (y . i) by A37, FUNCT_1: 47, FUNCT_4: 13;

              (z2 . i) = ((y | a2) . i) & ((y | a2) . i) = (y . i) by A35, A44, A48, FUNCT_1: 47, FUNCT_4: 13;

              hence (z . i) >= (z2 . i) by A49, YELLOW_0:def 1;

            end;

          end;

          hence thesis by WAYBEL_3: 28;

        end;

        then

        reconsider X as non empty directed Subset of L;

        now

          let i be Element of I;

          reconsider a = {i} as finite Subset of I by ZFMISC_1: 31;

          

           A50: (f +* (y | a)) in X;

          then

          reconsider z = (f +* (y | a)) as Element of L;

           ex_sup_of (X,L9) by WAYBEL_0: 75;

          then ( sup X) is_>=_than X by YELLOW_0: 30;

          then

           A51: z <= ( sup X) by A50;

          ( dom y) = I by WAYBEL_3: 27;

          then

           A52: ( dom (y | a)) = a by RELAT_1: 62;

          

           A53: i in a by TARSKI:def 1;

          then ((y | a) . i) = (y . i) by FUNCT_1: 49;

          then (z . i) = (y . i) by A53, A52, FUNCT_4: 13;

          hence (( sup X) . i) >= (y . i) by A51, WAYBEL_3: 28;

        end;

        then y <= ( sup X) by WAYBEL_3: 28;

        then

        consider d be Element of L such that

         A54: d in X and

         A55: x <= d by A2;

        consider a be finite Subset of I such that

         A56: d = (f +* (y | a)) by A54;

        K c= a

        proof

          ( dom y) = I by WAYBEL_3: 27;

          then

           A57: ( dom (y | a)) = a by RELAT_1: 62;

          let j be object;

          assume j in K;

          then

          consider i be Element of I such that

           A58: j = i and

           A59: (x . i) <> ( Bottom (J . i));

          (J . i) is up-complete lower-bounded non empty Poset by A1;

          then

           A60: (x . i) >= ( Bottom (J . i)) by YELLOW_0: 44;

          assume not j in a;

          

          then

           A61: (d . i) = (f . i) by A56, A58, A57, FUNCT_4: 11

          .= ( Bottom (J . i)) by A28;

          (x . i) <= (d . i) by A55, WAYBEL_3: 28;

          hence contradiction by A59, A61, A60, ORDERS_2: 2;

        end;

        then

        reconsider K as finite Subset of I;

        take K;

        thus for i be Element of I st not i in K holds (x . i) = ( Bottom (J . i));

      end;

      defpred P[ object, object] means ex i be Element of I, z be Element of L st $1 = i & $2 = z & (z . i) >= (x . i);

      assume

       A62: for i be Element of I holds (x . i) << (y . i);

      given K be finite Subset of I such that

       A63: for i be Element of I st not i in K holds (x . i) = ( Bottom (J . i));

      let D be non empty directed Subset of L such that

       A64: y <= ( sup D);

       A65:

      now

        let k be object;

        assume k in K;

        then

        reconsider i = k as Element of I;

        

         A66: ( pi (D,i)) is directed

        proof

          let a,b be Element of (J . i);

          assume a in ( pi (D,i));

          then

          consider f be Function such that

           A67: f in D and

           A68: a = (f . i) by CARD_3:def 6;

          assume b in ( pi (D,i));

          then

          consider g be Function such that

           A69: g in D and

           A70: b = (g . i) by CARD_3:def 6;

          reconsider f, g as Element of L by A67, A69;

          consider h be Element of L such that

           A71: h in D & h >= f & h >= g by A67, A69, WAYBEL_0:def 1;

          take (h . i);

          thus thesis by A68, A70, A71, CARD_3:def 6, WAYBEL_3: 28;

        end;

         ex_sup_of (D,L9) by WAYBEL_0: 75;

        then

         A72: (( sup D) . i) = ( sup ( pi (D,i))) by YELLOW16: 33;

        (x . i) << (y . i) & (y . i) <= (( sup D) . i) by A62, A64, WAYBEL_3: 28;

        then

        consider zi be Element of (J . i) such that

         A73: zi in ( pi (D,i)) and

         A74: zi >= (x . i) by A66, A72;

        consider a be Function such that

         A75: a in D and

         A76: zi = (a . i) by A73, CARD_3:def 6;

        reconsider a as object;

        take a;

        thus a in D by A75;

        thus P[k, a] by A74, A75, A76;

      end;

      consider F be Function such that

       A77: ( dom F) = K & ( rng F) c= D and

       A78: for k be object st k in K holds P[k, (F . k)] from FUNCT_1:sch 6( A65);

      reconsider Y = ( rng F) as finite Subset of D by A77, FINSET_1: 8;

      consider d be Element of L such that

       A79: d in D and

       A80: d is_>=_than Y by WAYBEL_0: 1;

      take d;

      thus d in D by A79;

      now

        let i be Element of I;

        

         A81: (J . i) is up-complete lower-bounded non empty Poset by A1;

        per cases ;

          suppose

           A82: i in K;

          then

          consider j be Element of I, z be Element of L such that

           A83: i = j and

           A84: (F . i) = z and

           A85: (z . j) >= (x . j) by A78;

          z in Y by A77, A82, A84, FUNCT_1:def 3;

          then d >= z by A80;

          then (d . i) >= (z . i) by WAYBEL_3: 28;

          hence (d . i) >= (x . i) by A81, A83, A85, YELLOW_0:def 2;

        end;

          suppose not i in K;

          then (x . i) = ( Bottom (J . i)) by A63;

          hence (d . i) >= (x . i) by A81, YELLOW_0: 44;

        end;

      end;

      hence thesis by WAYBEL_3: 28;

    end;

    registration

      let X be set;

      let L be lower-bounded non empty reflexive antisymmetric RelStr;

      cluster (L |^ X) -> lower-bounded;

      coherence

      proof

        

         A1: ( rng (X --> ( Bottom L))) c= the carrier of L;

        the carrier of (L |^ X) = ( Funcs (X,the carrier of L)) & ( dom (X --> ( Bottom L))) = X by YELLOW_1: 28;

        then

        reconsider f = (X --> ( Bottom L)) as Element of (L |^ X) by A1, FUNCT_2:def 2;

        take f;

        let g be Element of (L |^ X);

        per cases ;

          suppose

           A2: X is empty;

          

           A3: f <= f;

          (L |^ X) = RelStr (# { {} }, ( id { {} }) #) & f = {} by A2, YELLOW_1: 27;

          hence thesis by A3, TARSKI:def 1;

        end;

          suppose X is non empty;

          then

          reconsider X as non empty set;

          reconsider f, g as Element of (L |^ X);

          for x be Element of X holds (f . x) <= (g . x) by YELLOW_0: 44;

          hence thesis by WAYBEL27: 14;

        end;

      end;

    end

    registration

      let X be non empty TopSpace;

      let L be lower-bounded non empty TopPoset;

      cluster ( ContMaps (X,L)) -> lower-bounded;

      coherence

      proof

        reconsider f = (X --> ( Bottom L)) as Element of ( ContMaps (X,L)) by WAYBEL24: 21;

        take f;

        let g be Element of ( ContMaps (X,L));

        

         A1: ( ContMaps (X,L)) is full SubRelStr of (L |^ the carrier of X) by WAYBEL24:def 3;

        then

        reconsider a = g as Element of (L |^ the carrier of X) by YELLOW_0: 58;

        

         A2: the TopStruct of ( Omega X) = the TopStruct of X by WAYBEL25:def 2;

        

        then (( Omega X) --> ( Bottom L)) = (the carrier of X --> ( Bottom L))

        .= (X --> ( Bottom L));

        then a >= ( Bottom (L |^ the carrier of X)) & ( Bottom (L |^ the carrier of X)) = f by A2, WAYBEL24: 33, YELLOW_0: 44;

        hence thesis by A1, YELLOW_0: 60;

      end;

    end

    registration

      let L be up-complete non empty Poset;

      cluster -> up-complete for TopAugmentation of L;

      coherence

      proof

        let S be TopAugmentation of L;

         the RelStr of L = the RelStr of S by YELLOW_9:def 4;

        hence thesis by WAYBEL_8: 15;

      end;

      cluster Scott -> correct for TopAugmentation of L;

      coherence

      proof

        let IT be TopAugmentation of L;

        assume

         A1: IT is Scott;

        then ( [#] IT) is open;

        hence the carrier of IT in the topology of IT;

        thus for a be Subset-Family of IT st a c= the topology of IT holds ( union a) in the topology of IT

        proof

          let a be Subset-Family of IT;

          assume

           A2: a c= the topology of IT;

          

           A3: ( union a) is inaccessible

          proof

            let D be non empty directed Subset of IT;

            assume ( sup D) in ( union a);

            then

            consider A be set such that

             A4: ( sup D) in A and

             A5: A in a by TARSKI:def 4;

            reconsider A as Subset of IT by A5;

            A is open by A2, A5;

            then D meets A by A1, A4, WAYBEL11:def 1;

            then

            consider x be object such that

             A6: x in D and

             A7: x in A by XBOOLE_0: 3;

            x in ( union a) by A5, A7, TARSKI:def 4;

            hence thesis by A6, XBOOLE_0: 3;

          end;

          now

            let X be Subset of IT;

            assume X in a;

            then X is open by A2;

            hence X is upper by A1;

          end;

          then ( union a) is upper by WAYBEL_0: 28;

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

        end;

        thus for a,b be Subset of IT st a in the topology of IT & b in the topology of IT holds (a /\ b) in the topology of IT

        proof

          let a,b be Subset of IT;

          assume that

           A8: a in the topology of IT and

           A9: b in the topology of IT;

          reconsider a1 = a, b1 = b as Subset of IT;

          

           A10: b1 is open by A9;

          

           A11: a1 is open by A8;

          

           A12: (a /\ b) is inaccessible

          proof

            let D be non empty directed Subset of IT;

            assume

             A13: ( sup D) in (a /\ b);

            then ( sup D) in a1 by XBOOLE_0:def 4;

            then D meets a1 by A1, A11, WAYBEL11:def 1;

            then

            consider d1 be object such that

             A14: d1 in D and

             A15: d1 in a1 by XBOOLE_0: 3;

            ( sup D) in b1 by A13, XBOOLE_0:def 4;

            then D meets b1 by A1, A10, WAYBEL11:def 1;

            then

            consider d2 be object such that

             A16: d2 in D and

             A17: d2 in b1 by XBOOLE_0: 3;

            reconsider d1, d2 as Element of IT by A14, A16;

            consider z be Element of IT such that

             A18: z in D and

             A19: d1 <= z and

             A20: d2 <= z by A14, A16, WAYBEL_0:def 1;

            

             A21: z in b1 by A1, A10, A17, A20, WAYBEL_0:def 20;

            z in a1 by A1, A11, A15, A19, WAYBEL_0:def 20;

            then z in (a /\ b) by A21, XBOOLE_0:def 4;

            hence thesis by A18, XBOOLE_0: 3;

          end;

          (a /\ b) is upper by A1, A11, A10, WAYBEL_0: 29;

          hence thesis by A1, A12, PRE_TOPC:def 2;

        end;

      end;

    end

    registration

      let L be up-complete non empty Poset;

      cluster strict Scott for TopAugmentation of L;

      existence

      proof

        set T = { S where S be Subset of L : S is upper inaccessible };

        T c= ( bool the carrier of L)

        proof

          let x be object;

          assume x in T;

          then ex S be Subset of L st x = S & S is upper inaccessible;

          hence thesis;

        end;

        then

        reconsider T as Subset-Family of L;

        set SL = TopRelStr (# the carrier of L, the InternalRel of L, T #);

        

         A1: the RelStr of L = the RelStr of SL;

        then

        reconsider SL as TopAugmentation of L by YELLOW_9:def 4;

        take SL;

        for S be Subset of SL holds S is open iff S is inaccessible upper

        proof

          let S be Subset of SL;

          thus S is open implies S is inaccessible upper

          proof

            assume S is open;

            then S in T;

            then ex S1 be Subset of L st S1 = S & S1 is upper inaccessible;

            hence thesis by A1, WAYBEL_0: 25, YELLOW_9: 47;

          end;

          thus S is inaccessible upper implies S is open

          proof

            reconsider S1 = S as Subset of L;

            assume S is inaccessible upper;

            then S1 is inaccessible upper by A1, WAYBEL_0: 25, YELLOW_9: 47;

            then S in the topology of SL;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: WAYBEL29:13

    

     Th13: for L be up-complete non empty Poset holds for S1,S2 be Scott TopAugmentation of L holds the topology of S1 = the topology of S2

    proof

      let L be up-complete non empty Poset;

      let S1,S2 be Scott TopAugmentation of L;

      

       A1: the RelStr of S1 = the RelStr of L by YELLOW_9:def 4

      .= the RelStr of S2 by YELLOW_9:def 4;

      thus the topology of S1 c= the topology of S2

      proof

        let x be object;

        assume x in the topology of S1;

        then

        reconsider y = x as open Subset of S1 by PRE_TOPC:def 2;

        reconsider z = y as Subset of S2 by A1;

        z is inaccessible upper by A1, WAYBEL_0: 25, YELLOW_9: 47;

        hence thesis by PRE_TOPC:def 2;

      end;

      let x be object;

      assume x in the topology of S2;

      then

      reconsider y = x as open Subset of S2 by PRE_TOPC:def 2;

      reconsider z = y as Subset of S1 by A1;

      z is inaccessible upper by A1, WAYBEL_0: 25, YELLOW_9: 47;

      hence thesis by PRE_TOPC:def 2;

    end;

    theorem :: WAYBEL29:14

    

     Th14: for S1,S2 be up-complete antisymmetric non empty reflexive TopRelStr st the TopRelStr of S1 = the TopRelStr of S2 & S1 is Scott holds S2 is Scott

    proof

      let S1,S2 be up-complete antisymmetric non empty reflexive TopRelStr;

      assume

       A1: the TopRelStr of S1 = the TopRelStr of S2;

      assume

       A2: S1 is Scott;

      let T be Subset of S2;

      reconsider T1 = T as Subset of S1 by A1;

      

       A3: the RelStr of S1 = the RelStr of S2 by A1;

      thus T is open implies T is inaccessible upper

      proof

        assume T is open;

        then T in the topology of S2;

        then T1 is open by A1;

        hence thesis by A3, A2, WAYBEL_0: 25, YELLOW_9: 47;

      end;

      thus T is inaccessible upper implies T is open

      proof

        assume T is inaccessible upper;

        then T1 is inaccessible upper by A3, WAYBEL_0: 25, YELLOW_9: 47;

        then T1 in the topology of S1 by A2, PRE_TOPC:def 2;

        hence thesis by A1;

      end;

    end;

    definition

      let L be up-complete non empty Poset;

      :: WAYBEL29:def1

      func Sigma L -> strict Scott TopAugmentation of L means

      : Def1: not contradiction;

      uniqueness

      proof

        let S1,S2 be strict Scott TopAugmentation of L;

         the RelStr of S1 = the RelStr of L & the RelStr of S2 = the RelStr of L by YELLOW_9:def 4;

        hence thesis by Th13;

      end;

      existence ;

    end

    theorem :: WAYBEL29:15

    

     Th15: for S be Scott up-complete non empty TopPoset holds ( Sigma S) = the TopRelStr of S

    proof

      let S be Scott up-complete non empty TopPoset;

       the RelStr of the TopRelStr of S = the RelStr of S;

      then

      reconsider T = the TopRelStr of S as TopAugmentation of S by YELLOW_9:def 4;

      T is Scott by Th14;

      hence thesis by Def1;

    end;

    theorem :: WAYBEL29:16

    

     Th16: for L1,L2 be up-complete non empty Poset st the RelStr of L1 = the RelStr of L2 holds ( Sigma L1) = ( Sigma L2)

    proof

      let L1,L2 be up-complete non empty Poset;

      assume the RelStr of L1 = the RelStr of L2;

      then

       A1: the RelStr of ( Sigma L2) = the RelStr of L1 by YELLOW_9:def 4;

      then the RelStr of ( Sigma L1) = the RelStr of L1 & ( Sigma L2) is TopAugmentation of L1 by YELLOW_9:def 4;

      hence thesis by A1, Th13;

    end;

    definition

      let S,T be up-complete non empty Poset;

      let f be Function of S, T;

      :: WAYBEL29:def2

      func Sigma f -> Function of ( Sigma S), ( Sigma T) equals f;

      coherence

      proof

         the RelStr of ( Sigma S) = the RelStr of S & the RelStr of ( Sigma T) = the RelStr of T by YELLOW_9:def 4;

        hence thesis;

      end;

    end

    registration

      let S,T be up-complete non empty Poset;

      let f be directed-sups-preserving Function of S, T;

      cluster ( Sigma f) -> continuous;

      coherence

      proof

         the RelStr of ( Sigma S) = the RelStr of S & the RelStr of ( Sigma T) = the RelStr of T by YELLOW_9:def 4;

        hence thesis by WAYBEL17: 29, WAYBEL21: 6;

      end;

    end

    theorem :: WAYBEL29:17

    for S,T be up-complete non empty Poset holds for f be Function of S, T holds f is isomorphic iff ( Sigma f) is isomorphic

    proof

      let S,T be up-complete non empty Poset;

      let f be Function of S, T;

       the RelStr of ( Sigma S) = the RelStr of S & the RelStr of ( Sigma T) = the RelStr of T by YELLOW_9:def 4;

      hence thesis by Th5;

    end;

    theorem :: WAYBEL29:18

    

     Th18: for X be non empty TopSpace holds for S be Scott complete TopLattice holds ( oContMaps (X,S)) = ( ContMaps (X,S))

    proof

      let X be non empty TopSpace;

      let S be Scott complete TopLattice;

      

       A1: ( Omega S) = the TopRelStr of S & the TopStruct of X = the TopStruct of X by WAYBEL25: 15;

      

      thus ( oContMaps (X,S)) = ( ContMaps (X,( Omega S))) by WAYBEL26:def 1

      .= ( ContMaps (X,S)) by A1, Th10;

    end;

    definition

      let X,Y be non empty TopSpace;

      :: WAYBEL29:def3

      func Theta (X,Y) -> Function of ( InclPoset the topology of [:X, Y:]), ( ContMaps (X,( Sigma ( InclPoset the topology of Y)))) means

      : Def3: for W be open Subset of [:X, Y:] holds (it . W) = ((W,the carrier of X) *graph );

      existence

      proof

        ( Omega ( Sigma ( InclPoset the topology of Y))) = ( Sigma ( InclPoset the topology of Y)) by WAYBEL25: 15;

        then (ex F be Function of ( InclPoset the topology of [:X, Y:]), ( oContMaps (X,( Sigma ( InclPoset the topology of Y)))) st F is monotone & for W be open Subset of [:X, Y:] holds (F . W) = ((W,the carrier of X) *graph )) & ( oContMaps (X,( Sigma ( InclPoset the topology of Y)))) = ( ContMaps (X,( Sigma ( InclPoset the topology of Y)))) by WAYBEL26: 45, WAYBEL26:def 1;

        hence thesis;

      end;

      correctness

      proof

        let F,G be Function of ( InclPoset the topology of [:X, Y:]), ( ContMaps (X,( Sigma ( InclPoset the topology of Y)))) such that

         A1: for W be open Subset of [:X, Y:] holds (F . W) = ((W,the carrier of X) *graph ) and

         A2: for W be open Subset of [:X, Y:] holds (G . W) = ((W,the carrier of X) *graph );

        now

          let x be Element of ( InclPoset the topology of [:X, Y:]);

          the carrier of ( InclPoset the topology of [:X, Y:]) = the topology of [:X, Y:] by YELLOW_1: 1;

          then x in the topology of [:X, Y:];

          then

          reconsider W = x as open Subset of [:X, Y:] by PRE_TOPC:def 2;

          

          thus (F . x) = ((W,the carrier of X) *graph ) by A1

          .= (G . x) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    defpred a4101[ T_0-TopSpace] means for X be non empty TopSpace holds for L be Scott continuous complete TopLattice holds for T be Scott TopAugmentation of ( ContMaps ($1,L)) holds ex f be Function of ( ContMaps (X,T)), ( ContMaps ( [:X, $1:],L)), g be Function of ( ContMaps ( [:X, $1:],L)), ( ContMaps (X,T)) st f is uncurrying one-to-one onto & g is currying one-to-one onto;

    defpred a41019[ T_0-TopSpace] means for X be non empty TopSpace holds for L be Scott continuous complete TopLattice holds for T be Scott TopAugmentation of ( ContMaps ($1,L)) holds ex f be Function of ( ContMaps (X,T)), ( ContMaps ( [:X, $1:],L)), g be Function of ( ContMaps ( [:X, $1:],L)), ( ContMaps (X,T)) st f is uncurrying isomorphic & g is currying isomorphic;

    defpred a4102[ T_0-TopSpace] means for X be non empty TopSpace holds ( Theta (X,$1)) is isomorphic;

    defpred a4103[ T_0-TopSpace] means for X be non empty TopSpace holds for T be Scott TopAugmentation of ( InclPoset the topology of $1) holds for f be continuous Function of X, T holds ( *graph f) is open Subset of [:X, $1:];

    defpred a4104[ T_0-TopSpace] means for T be Scott TopAugmentation of ( InclPoset the topology of $1) holds { [W, y] where W be open Subset of $1, y be Element of $1 : y in W } is open Subset of [:T, $1:];

    defpred a4105[ T_0-TopSpace] means for S be Scott TopAugmentation of ( InclPoset the topology of $1) holds for y be Element of $1, V be open a_neighborhood of y holds ex H be open Subset of S st V in H & ( meet H) is a_neighborhood of y;

    

     Lm1: for T be T_0-TopSpace holds a4101[T] iff a41019[T]

    proof

      let T be T_0-TopSpace;

      thus a4101[T] implies a41019[T]

      proof

        assume

         A1: a4101[T];

        let X be non empty TopSpace;

        let L be Scott continuous complete TopLattice;

        let S be Scott TopAugmentation of ( ContMaps (T,L));

        consider f be Function of ( ContMaps (X,S)), ( ContMaps ( [:X, T:],L)), g be Function of ( ContMaps ( [:X, T:],L)), ( ContMaps (X,S)) such that

         A2: f is uncurrying one-to-one onto and

         A3: g is currying one-to-one onto by A1;

        

         A4: the RelStr of S = the RelStr of ( ContMaps (T,L)) by YELLOW_9:def 4;

        

         A5: ( ContMaps (T,L)) is full non empty SubRelStr of (L |^ the carrier of T) by WAYBEL24:def 3;

        then

         A6: the InternalRel of ( ContMaps (T,L)) = (the InternalRel of (L |^ the carrier of T) |_2 the carrier of ( ContMaps (T,L))) by YELLOW_0:def 14;

        the carrier of ( ContMaps (T,L)) c= the carrier of (L |^ the carrier of T) & the InternalRel of ( ContMaps (T,L)) c= the InternalRel of (L |^ the carrier of T) by A5, YELLOW_0:def 13;

        then S is full non empty SubRelStr of (L |^ the carrier of T) by A4, A6, YELLOW_0:def 13, YELLOW_0:def 14;

        then

         A7: (S |^ the carrier of X) is full non empty SubRelStr of ((L |^ the carrier of T) |^ the carrier of X) by YELLOW16: 39;

        (L |^ the carrier of [:X, T:]) = (L |^ [:the carrier of X, the carrier of T:]) by BORSUK_1:def 2;

        then

         A8: ( ContMaps ( [:X, T:],L)) is full non empty SubRelStr of (L |^ [:the carrier of X, the carrier of T:]) by WAYBEL24:def 3;

        ( ContMaps (X,S)) is full non empty SubRelStr of (S |^ the carrier of X) by WAYBEL24:def 3;

        then ( ContMaps (X,S)) is full non empty SubRelStr of ((L |^ the carrier of T) |^ the carrier of X) by A7, WAYBEL15: 1;

        then

         A9: f is monotone & g is monotone by A2, A3, A8, WAYBEL27: 20, WAYBEL27: 21;

        take f, g;

        ( ContMaps (T,L)) is full non empty SubRelStr of (L |^ the carrier of T) by WAYBEL24:def 3;

        then (( ContMaps (T,L)) |^ the carrier of X) is full SubRelStr of ((L |^ the carrier of T) |^ the carrier of X) by YELLOW16: 39;

        then

         A10: the carrier of (( ContMaps (T,L)) |^ the carrier of X) c= the carrier of ((L |^ the carrier of T) |^ the carrier of X) by YELLOW_0:def 13;

        

         A11: ( rng f) = the carrier of ( ContMaps ( [:X, T:],L)) by A2, FUNCT_2:def 3

        .= ( dom g) by FUNCT_2:def 1;

        ( ContMaps (X,S)) is non empty full SubRelStr of (S |^ the carrier of X) by WAYBEL24:def 3;

        then the carrier of ( ContMaps (X,S)) c= the carrier of (S |^ the carrier of X) by YELLOW_0:def 13;

        then ( dom f) c= the carrier of (S |^ the carrier of X);

        then ( dom f) c= the carrier of (( ContMaps (T,L)) |^ the carrier of X) by A4, WAYBEL27: 15;

        then ( dom f) c= the carrier of ((L |^ the carrier of T) |^ the carrier of X) by A10;

        then ( dom f) c= ( Funcs (the carrier of X,the carrier of (L |^ the carrier of T))) by YELLOW_1: 28;

        then ( dom f) c= ( Funcs (the carrier of X,( Funcs (the carrier of T,the carrier of L)))) by YELLOW_1: 28;

        then (g * f) = ( id ( dom f)) by A2, A3, A11, WAYBEL27: 4;

        then g = (f qua Function " ) by A2, A11, FUNCT_1: 41;

        hence f is uncurrying isomorphic by A2, A9, WAYBEL_0:def 38;

        

         A12: ( rng g) = the carrier of ( ContMaps (X,S)) by A3, FUNCT_2:def 3

        .= ( dom f) by FUNCT_2:def 1;

        ( ContMaps ( [:X, T:],L)) is non empty full SubRelStr of (L |^ the carrier of [:X, T:]) by WAYBEL24:def 3;

        then the carrier of ( ContMaps ( [:X, T:],L)) c= the carrier of (L |^ the carrier of [:X, T:]) by YELLOW_0:def 13;

        then ( dom g) c= the carrier of (L |^ the carrier of [:X, T:]);

        then ( dom g) c= ( Funcs (the carrier of [:X, T:],the carrier of L)) by YELLOW_1: 28;

        then ( dom g) c= ( Funcs ( [:the carrier of X, the carrier of T:],the carrier of L)) by BORSUK_1:def 2;

        then (f * g) = ( id ( dom g)) by A2, A3, A12, WAYBEL27: 5;

        then f = (g qua Function " ) by A3, A12, FUNCT_1: 41;

        hence thesis by A3, A9, WAYBEL_0:def 38;

      end;

      assume

       A13: a41019[T];

      let X be non empty TopSpace;

      let L be Scott continuous complete TopLattice;

      let S be Scott TopAugmentation of ( ContMaps (T,L));

      consider f be Function of ( ContMaps (X,S)), ( ContMaps ( [:X, T:],L)), g be Function of ( ContMaps ( [:X, T:],L)), ( ContMaps (X,S)) such that

       A14: f is uncurrying isomorphic and

       A15: g is currying isomorphic by A13;

      take f, g;

      thus f is uncurrying one-to-one onto by A14;

      thus thesis by A15;

    end;

    begin

    definition

      let X be non empty TopSpace;

      :: WAYBEL29:def4

      func alpha X -> Function of ( oContMaps (X, Sierpinski_Space )), ( InclPoset the topology of X) means

      : Def4: for g be continuous Function of X, Sierpinski_Space holds (it . g) = (g " {1});

      existence

      proof

        deffunc F( Function) = ($1 " {1});

        consider f be Function such that

         A1: ( dom f) = the carrier of ( oContMaps (X, Sierpinski_Space )) and

         A2: for x be Element of ( oContMaps (X, Sierpinski_Space )) holds (f . x) = F(x) from FUNCT_1:sch 4;

        ( rng f) c= the topology of X

        proof

          the topology of Sierpinski_Space = { {} , {1}, { 0 , 1}} by WAYBEL18:def 9;

          then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;

          then

          reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def 2;

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A3: x in ( dom f) and

           A4: y = (f . x) by FUNCT_1:def 3;

          reconsider x as Element of ( oContMaps (X, Sierpinski_Space )) by A1, A3;

          reconsider g = x as continuous Function of X, Sierpinski_Space by WAYBEL26: 2;

          ( [#] Sierpinski_Space ) <> {} ;

          then

           A5: (g " A) is open by TOPS_2: 43;

          y = (g " A) by A2, A4;

          hence thesis by A5;

        end;

        then ( rng f) c= the carrier of ( InclPoset the topology of X) by YELLOW_1: 1;

        then

        reconsider f as Function of ( oContMaps (X, Sierpinski_Space )), ( InclPoset the topology of X) by A1, FUNCT_2: 2;

        take f;

        let g be continuous Function of X, Sierpinski_Space ;

        g is Element of ( oContMaps (X, Sierpinski_Space )) by WAYBEL26: 2;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( oContMaps (X, Sierpinski_Space )), ( InclPoset the topology of X) such that

         A6: for g be continuous Function of X, Sierpinski_Space holds (f1 . g) = (g " {1}) and

         A7: for g be continuous Function of X, Sierpinski_Space holds (f2 . g) = (g " {1});

        now

          let x be Element of ( oContMaps (X, Sierpinski_Space ));

          reconsider g = x as continuous Function of X, Sierpinski_Space by WAYBEL26: 2;

          

          thus (f1 . x) = (g " {1}) by A6

          .= (f2 . x) by A7;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: WAYBEL29:19

    for X be non empty TopSpace holds for V be open Subset of X holds ((( alpha X) " ) . V) = ( chi (V,the carrier of X))

    proof

      

       A1: the carrier of Sierpinski_Space = { 0 , 1} by WAYBEL18:def 9;

      the topology of Sierpinski_Space = { {} , {1}, { 0 , 1}} by WAYBEL18:def 9;

      then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;

      then

      reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def 2;

      let X be non empty TopSpace;

      consider f be Function of ( InclPoset the topology of X), ( oContMaps (X, Sierpinski_Space )) such that

       A2: f is isomorphic and

       A3: for V be open Subset of X holds (f . V) = ( chi (V,the carrier of X)) by WAYBEL26: 5;

      

       A4: the carrier of ( InclPoset the topology of X) = the topology of X by YELLOW_1: 1;

      

       A5: ( rng f) = ( [#] ( oContMaps (X, Sierpinski_Space ))) by A2, WAYBEL_0: 66;

      

       A6: (f " ) = (f qua Function " ) by A2, TOPS_2:def 4;

      now

        let x be Element of ( oContMaps (X, Sierpinski_Space ));

        reconsider g = x as continuous Function of X, Sierpinski_Space by WAYBEL26: 2;

        ( [#] Sierpinski_Space ) <> {} ;

        then

         A7: (g " A) is open by TOPS_2: 43;

        then

         A8: (g " A) in the topology of X;

        

         A9: (f . (g " A)) = ( chi ((g " A),the carrier of X)) by A3, A7

        .= x by A1, FUNCT_3: 40;

        

        thus (( alpha X) . x) = (g " A) by Def4

        .= ((f " ) . x) by A2, A6, A4, A8, A9, FUNCT_2: 26;

      end;

      then ( alpha X) = (f " ) by FUNCT_2: 63;

      then (( alpha X) " ) = f by A2, A5, TOPS_2: 51;

      hence thesis by A3;

    end;

    registration

      let X be non empty TopSpace;

      cluster ( alpha X) -> isomorphic;

      coherence

      proof

        the topology of Sierpinski_Space = { {} , {1}, { 0 , 1}} by WAYBEL18:def 9;

        then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;

        then

        reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def 2;

        consider f be Function of ( InclPoset the topology of X), ( oContMaps (X, Sierpinski_Space )) such that

         A1: f is isomorphic and

         A2: for V be open Subset of X holds (f . V) = ( chi (V,the carrier of X)) by WAYBEL26: 5;

        

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

        

         A4: the carrier of ( InclPoset the topology of X) = the topology of X by YELLOW_1: 1;

        

         A5: the carrier of Sierpinski_Space = { 0 , 1} by WAYBEL18:def 9;

        now

          let x be Element of ( oContMaps (X, Sierpinski_Space ));

          reconsider g = x as continuous Function of X, Sierpinski_Space by WAYBEL26: 2;

          ( [#] Sierpinski_Space ) <> {} ;

          then

           A6: (g " A) is open by TOPS_2: 43;

          then

           A7: (g " A) in the topology of X;

          

           A8: (f . (g " A)) = ( chi ((g " A),the carrier of X)) by A2, A6

          .= x by A5, FUNCT_3: 40;

          

          thus (( alpha X) . x) = (g " A) by Def4

          .= ((f " ) . x) by A1, A3, A4, A7, A8, FUNCT_2: 26;

        end;

        hence thesis by A1, A3, FUNCT_2: 63, WAYBEL_0: 68;

      end;

    end

    registration

      let X be non empty TopSpace;

      cluster (( alpha X) " ) -> isomorphic;

      coherence by YELLOW14: 10;

    end

    registration

      let S be injective T_0-TopSpace;

      cluster ( Omega S) -> Scott;

      coherence

      proof

        set T = the strict Scott TopAugmentation of ( Omega S);

        

         A1: the TopStruct of T = the TopStruct of S by WAYBEL25: 37

        .= the TopStruct of ( Omega S) by WAYBEL25:def 2;

         the RelStr of T = the RelStr of ( Omega S) by YELLOW_9:def 4;

        hence thesis by A1;

      end;

    end

    registration

      let X be non empty TopSpace;

      cluster ( oContMaps (X, Sierpinski_Space )) -> complete;

      coherence

      proof

        (( InclPoset the topology of X),( oContMaps (X, Sierpinski_Space ))) are_isomorphic by WAYBEL26: 6;

        hence thesis by WAYBEL20: 18;

      end;

    end

    theorem :: WAYBEL29:20

    ( Omega Sierpinski_Space ) = ( Sigma ( BoolePoset { 0 }))

    proof

      set S = ( Sigma ( BoolePoset { 0 }));

      reconsider T = ( Omega Sierpinski_Space ) as Scott strict TopAugmentation of ( BoolePoset { 0 }) by WAYBEL26: 4;

      

       A1: the topology of T = ( sigma ( BoolePoset { 0 })) by YELLOW_9: 51

      .= the topology of S by YELLOW_9: 51;

       the RelStr of T = ( BoolePoset { 0 }) by YELLOW_9:def 4

      .= the RelStr of S by YELLOW_9:def 4;

      hence thesis by A1;

    end;

    registration

      let M be non empty set;

      let S be injective T_0-TopSpace;

      cluster (M -TOP_prod (M => S)) -> injective;

      coherence

      proof

        for m be Element of M holds ((M => S) . m) is injective;

        hence thesis by WAYBEL18: 7;

      end;

    end

    theorem :: WAYBEL29:21

    for M be non empty set, L be complete continuous LATTICE holds ( Omega (M -TOP_prod (M => ( Sigma L)))) = ( Sigma (M -POS_prod (M => L)))

    proof

      let M be non empty set, L be complete continuous LATTICE;

      

       A1: the RelStr of ( Sigma L) = the RelStr of L by YELLOW_9:def 4;

      reconsider S = ( Sigma L) as injective T_0-TopSpace;

      ( Omega ( Sigma L)) = ( Sigma L) by WAYBEL25: 15;

      

      then the RelStr of ( Omega (M -TOP_prod (M => ( Sigma L)))) = (M -POS_prod (M => ( Sigma L))) by WAYBEL25: 14

      .= (( Sigma L) |^ M) by YELLOW_1:def 5

      .= (L |^ M) by A1, WAYBEL27: 15;

      

      then ( Sigma (L |^ M)) = ( Sigma ( Omega (M -TOP_prod (M => S)))) by Th16

      .= ( Omega (M -TOP_prod (M => ( Sigma L)))) by Th15;

      hence thesis by YELLOW_1:def 5;

    end;

    theorem :: WAYBEL29:22

    for M be non empty set, T be injective T_0-TopSpace holds ( Omega (M -TOP_prod (M => T))) = ( Sigma (M -POS_prod (M => ( Omega T))))

    proof

      let M be non empty set, T be injective T_0-TopSpace;

      set L = ( Omega T);

       the RelStr of ( Omega (M -TOP_prod (M => T))) = (M -POS_prod (M => L)) by WAYBEL25: 14;

      then ( Sigma ( Omega (M -TOP_prod (M => T)))) = ( Sigma (M -POS_prod (M => L))) by Th16;

      hence thesis by Th15;

    end;

    definition

      let M be non empty set;

      let X,Y be non empty TopSpace;

      :: WAYBEL29:def5

      func commute (X,M,Y) -> Function of ( oContMaps (X,(M -TOP_prod (M => Y)))), (( oContMaps (X,Y)) |^ M) means

      : Def5: for f be continuous Function of X, (M -TOP_prod (M => Y)) holds (it . f) = ( commute f);

      uniqueness

      proof

        let F1,F2 be Function of ( oContMaps (X,(M -TOP_prod (M => Y)))), (( oContMaps (X,Y)) |^ M) such that

         A1: for f be continuous Function of X, (M -TOP_prod (M => Y)) holds (F1 . f) = ( commute f) and

         A2: for f be continuous Function of X, (M -TOP_prod (M => Y)) holds (F2 . f) = ( commute f);

        now

          let f be Element of ( oContMaps (X,(M -TOP_prod (M => Y))));

          reconsider g = f as continuous Function of X, (M -TOP_prod (M => Y)) by WAYBEL26: 2;

          

          thus (F1 . f) = ( commute g) by A1

          .= (F2 . f) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      existence

      proof

        deffunc F( Function) = ( commute $1);

        consider F be Function such that

         A3: ( dom F) = the carrier of ( oContMaps (X,(M -TOP_prod (M => Y)))) and

         A4: for f be Element of ( oContMaps (X,(M -TOP_prod (M => Y)))) holds (F . f) = F(f) from FUNCT_1:sch 4;

        ( rng F) c= the carrier of (( oContMaps (X,Y)) |^ M)

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider x be object such that

           A5: x in ( dom F) and

           A6: y = (F . x) by FUNCT_1:def 3;

          reconsider x as Element of ( oContMaps (X,(M -TOP_prod (M => Y)))) by A3, A5;

          reconsider f = x as continuous Function of X, (M -TOP_prod (M => Y)) by WAYBEL26: 2;

          ( commute f) is Function of M, the carrier of ( oContMaps (X,Y)) & y = ( commute x) by A4, A6, WAYBEL26: 31;

          then y in ( Funcs (M,the carrier of ( oContMaps (X,Y)))) by FUNCT_2: 8;

          hence thesis by YELLOW_1: 28;

        end;

        then

        reconsider F as Function of ( oContMaps (X,(M -TOP_prod (M => Y)))), (( oContMaps (X,Y)) |^ M) by A3, FUNCT_2: 2;

        take F;

        let f be continuous Function of X, (M -TOP_prod (M => Y));

        f is Element of ( oContMaps (X,(M -TOP_prod (M => Y)))) by WAYBEL26: 2;

        hence thesis by A4;

      end;

    end

    registration

      let M be non empty set;

      let X,Y be non empty TopSpace;

      cluster ( commute (X,M,Y)) -> one-to-one onto;

      correctness

      proof

        set f = ( commute (X,M,Y));

        ( Carrier (M => Y)) = (M => the carrier of Y) by WAYBEL26: 30;

        

        then the carrier of (M -TOP_prod (M => Y)) = ( product (M => the carrier of Y)) by WAYBEL18:def 3

        .= ( Funcs (M,the carrier of Y)) by CARD_3: 11;

        then

         A1: the carrier of ( oContMaps (X,(M -TOP_prod (M => Y)))) c= ( Funcs (the carrier of X,( Funcs (M,the carrier of Y)))) by WAYBEL26: 32;

        now

          thus the carrier of (( oContMaps (X,Y)) |^ M) <> {} ;

          let x1,x2 be object;

          assume that

           A2: x1 in the carrier of ( oContMaps (X,(M -TOP_prod (M => Y)))) and

           A3: x2 in the carrier of ( oContMaps (X,(M -TOP_prod (M => Y))));

          reconsider a1 = x1, a2 = x2 as Element of ( oContMaps (X,(M -TOP_prod (M => Y)))) by A2, A3;

          reconsider f1 = a1, f2 = a2 as continuous Function of X, (M -TOP_prod (M => Y)) by WAYBEL26: 2;

          assume (f . x1) = (f . x2);

          

          then ( commute f1) = (f . x2) by Def5

          .= ( commute f2) by Def5;

          then f1 = ( commute ( commute f2)) by A1, FUNCT_6: 57;

          hence x1 = x2 by A1, FUNCT_6: 57;

        end;

        hence ( commute (X,M,Y)) is one-to-one;

        ( rng f) = the carrier of (( oContMaps (X,Y)) |^ M)

        proof

          thus ( rng f) c= the carrier of (( oContMaps (X,Y)) |^ M);

          let x be object;

          assume x in the carrier of (( oContMaps (X,Y)) |^ M);

          then

          reconsider x as Element of (( oContMaps (X,Y)) |^ M);

          

           A4: the carrier of (( oContMaps (X,Y)) |^ M) = ( Funcs (M,the carrier of ( oContMaps (X,Y)))) by YELLOW_1: 28;

          then

          reconsider x as Function of M, the carrier of ( oContMaps (X,Y)) by FUNCT_2: 66;

          reconsider g = ( commute x) as continuous Function of X, (M -TOP_prod (M => Y)) by WAYBEL26: 33;

          reconsider y = g as Element of ( oContMaps (X,(M -TOP_prod (M => Y)))) by WAYBEL26: 2;

          the carrier of (( oContMaps (X,Y)) |^ M) c= ( Funcs (M,( Funcs (the carrier of X,the carrier of Y)))) by A4, FUNCT_5: 56, WAYBEL26: 32;

          then ( commute ( commute x)) = x by FUNCT_6: 57;

          then

           A5: (f . y) = x by Def5;

          ( dom f) = the carrier of ( oContMaps (X,(M -TOP_prod (M => Y)))) by FUNCT_2:def 1;

          hence thesis by A5, FUNCT_1:def 3;

        end;

        hence thesis by FUNCT_2:def 3;

      end;

    end

    registration

      let M be non empty set;

      let X be non empty TopSpace;

      cluster ( commute (X,M, Sierpinski_Space )) -> isomorphic;

      correctness

      proof

        (M -POS_prod (M => ( oContMaps (X, Sierpinski_Space )))) = (( oContMaps (X, Sierpinski_Space )) |^ M) by YELLOW_1:def 5;

        then ex f1 be Function of ( oContMaps (X,(M -TOP_prod (M => Sierpinski_Space )))), (( oContMaps (X, Sierpinski_Space )) |^ M) st f1 is isomorphic & for f be continuous Function of X, (M -TOP_prod (M => Sierpinski_Space )) holds (f1 . f) = ( commute f) by WAYBEL26: 34;

        hence thesis by Def5;

      end;

    end

    

     Lm2: for T be T_0-TopSpace st a4102[T] holds a4103[T]

    proof

      let Y be T_0-TopSpace such that

       A1: a4102[Y];

      set S = ( Sigma ( InclPoset the topology of Y));

      let X be non empty TopSpace;

      let T be Scott TopAugmentation of ( InclPoset the topology of Y);

      

       A2: the topology of T = ( sigma ( InclPoset the topology of Y)) by YELLOW_9: 51;

      let f be continuous Function of X, T;

       the RelStr of T = ( InclPoset the topology of Y) & the RelStr of S = ( InclPoset the topology of Y) by YELLOW_9:def 4;

      then

       A3: the TopStruct of X = the TopStruct of X & the TopRelStr of T = the TopRelStr of S by A2, YELLOW_9: 51;

      then

      reconsider F = ( Theta (X,Y)) as Function of ( InclPoset the topology of [:X, Y:]), ( ContMaps (X,T)) by Th10;

      ( ContMaps (X,T)) = ( ContMaps (X,S)) by A3, Th10;

      then F is isomorphic by A1;

      then f in the carrier of ( ContMaps (X,T)) & ( rng F) = the carrier of ( ContMaps (X,T)) by WAYBEL24:def 3, WAYBEL_0: 66;

      then

      consider W be object such that

       A4: W in ( dom F) and

       A5: f = (F . W) by FUNCT_1:def 3;

      ( dom F) = the carrier of ( InclPoset the topology of [:X, Y:]) by FUNCT_2:def 1

      .= the topology of [:X, Y:] by YELLOW_1: 1;

      then

      reconsider W as open Subset of [:X, Y:] by A4, PRE_TOPC:def 2;

      reconsider R = W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def 2;

      

       A6: ( dom R) c= the carrier of X;

      f = ((W,the carrier of X) *graph ) by A5, Def3;

      hence thesis by A6, WAYBEL26: 41;

    end;

    theorem :: WAYBEL29:23

    

     Th23: for X,Y be non empty TopSpace holds for S be Scott TopAugmentation of ( InclPoset the topology of Y) holds for f1,f2 be Element of ( ContMaps (X,S)) st f1 <= f2 holds ( *graph f1) c= ( *graph f2)

    proof

      let X,Y be non empty TopSpace;

      let S be Scott TopAugmentation of ( InclPoset the topology of Y);

      let f1,f2 be Element of ( ContMaps (X,S));

      assume

       A1: f1 <= f2;

      reconsider F1 = f1, F2 = f2 as Function of X, S by WAYBEL24: 21;

      let a,b be object;

      

       A2: the RelStr of S = the RelStr of ( InclPoset the topology of Y) by YELLOW_9:def 4;

      f2 is Function of X, S by WAYBEL24: 21;

      then

       A3: ( dom f2) = the carrier of X by FUNCT_2:def 1;

      assume

       A4: [a, b] in ( *graph f1);

      then

       A5: a in ( dom f1) & b in (f1 . a) by WAYBEL26: 38;

      f1 is Function of X, S by WAYBEL24: 21;

      then

       A6: ( dom f1) = the carrier of X by FUNCT_2:def 1;

      then

      reconsider a9 = a as Element of X by A4, WAYBEL26: 38;

      (F1 . a9) is Element of S;

      then (f1 . a) in the carrier of ( InclPoset the topology of Y) by A2;

      then

       A7: (f1 . a) in the topology of Y by YELLOW_1: 1;

      (F2 . a9) is Element of S;

      then (f2 . a) in the carrier of ( InclPoset the topology of Y) by A2;

      then

       A8: (f2 . a) in the topology of Y by YELLOW_1: 1;

       [(f1 . a9), (f2 . a9)] in the InternalRel of S by A1, WAYBEL24: 20;

      then [(f1 . a), (f2 . a)] in ( RelIncl the topology of Y) by A2, YELLOW_1: 1;

      then (f1 . a) c= (f2 . a) by A7, A8, WELLORD2:def 1;

      hence thesis by A6, A3, A5, WAYBEL26: 38;

    end;

    

     Lm3: for T be T_0-TopSpace st a4103[T] holds a4102[T]

    proof

      deffunc F( Function) = ( *graph $1);

      let Y be T_0-TopSpace such that

       A1: a4103[Y];

      set T = ( Sigma ( InclPoset the topology of Y));

      let X be non empty TopSpace;

      consider G be Function such that

       A2: ( dom G) = the carrier of ( ContMaps (X,T)) and

       A3: for f be Element of ( ContMaps (X,T)) holds (G . f) = F(f) from FUNCT_1:sch 4;

      ( rng G) c= the carrier of ( InclPoset the topology of [:X, Y:])

      proof

        let x be object;

        assume x in ( rng G);

        then

        consider a be object such that

         A4: a in ( dom G) and

         A5: x = (G . a) by FUNCT_1:def 3;

        reconsider a as Element of ( ContMaps (X,T)) by A2, A4;

        reconsider a as continuous Function of X, T by WAYBEL24: 21;

        x = ( *graph a) by A3, A5;

        then x is open Subset of [:X, Y:] by A1;

        then x in the topology of [:X, Y:] by PRE_TOPC:def 2;

        hence thesis by YELLOW_1: 1;

      end;

      then

      reconsider G as Function of ( ContMaps (X,T)), ( InclPoset the topology of [:X, Y:]) by A2, FUNCT_2: 2;

      consider F be Function of ( InclPoset the topology of [:X, Y:]), ( oContMaps (X,T)) such that

       A6: F is monotone and

       A7: for W be open Subset of [:X, Y:] holds (F . W) = ((W,the carrier of X) *graph ) by WAYBEL26: 45;

      

       A8: G is monotone

      proof

        let f1,f2 be Element of ( ContMaps (X,T));

        assume f1 <= f2;

        then ( *graph f1) c= ( *graph f2) by Th23;

        then (G . f1) c= ( *graph f2) by A3;

        then (G . f1) c= (G . f2) by A3;

        hence (G . f1) <= (G . f2) by YELLOW_1: 3;

      end;

      reconsider F as Function of ( InclPoset the topology of [:X, Y:]), ( ContMaps (X,T)) by Th18;

      ( dom F) = the carrier of ( InclPoset the topology of [:X, Y:]) by FUNCT_2:def 1;

      then ( rng G) c= ( dom F);

      then

       A9: ( dom (F * G)) = the carrier of ( ContMaps (X,T)) by A2, RELAT_1: 27;

      now

        let x be object;

        assume

         A10: x in the carrier of ( ContMaps (X,T));

        then

        reconsider x1 = x as continuous Function of X, T by WAYBEL24: 21;

        reconsider gx = ( *graph x1) as open Subset of [:X, Y:] by A1;

        

         A11: ( dom x1) = the carrier of X by FUNCT_2:def 1;

         A12:

        now

          let i be object;

          assume i in the carrier of X;

          then

           A13: i in ( dom x1) by FUNCT_2:def 1;

          

           A14: i in {i} by TARSKI:def 1;

          thus (x1 . i) = ( Im (gx,i))

          proof

            thus (x1 . i) c= ( Im (gx,i))

            proof

              let b be object;

              assume b in (x1 . i);

              then [i, b] in gx by A13, WAYBEL26: 38;

              hence thesis by A14, RELAT_1:def 13;

            end;

            let b be object;

            assume b in ( Im (gx,i));

            then ex j be object st [j, b] in gx & j in {i} by RELAT_1:def 13;

            then [i, b] in gx by TARSKI:def 1;

            hence thesis by WAYBEL26: 38;

          end;

        end;

        ((F * G) . x) = (F . (G . x1)) by A9, A10, FUNCT_1: 12

        .= (F . gx) by A3, A10

        .= ((gx,the carrier of X) *graph ) by A7;

        hence ((F * G) . x) = x by A11, A12, WAYBEL26:def 5;

      end;

      then

       A15: (F * G) = ( id ( ContMaps (X,T))) by A9, FUNCT_1: 17;

      

       A16: ( dom (G * F)) = the carrier of ( InclPoset the topology of [:X, Y:]) by FUNCT_2:def 1;

      now

        let x be object;

        assume

         A17: x in the carrier of ( InclPoset the topology of [:X, Y:]);

        then x in the topology of [:X, Y:] by YELLOW_1: 1;

        then

        reconsider x1 = x as open Subset of [:X, Y:] by PRE_TOPC:def 2;

        ((x1,the carrier of X) *graph ) is continuous Function of X, T by WAYBEL26: 43;

        then

        reconsider x1X = ((x1,the carrier of X) *graph ) as Element of ( ContMaps (X,T)) by WAYBEL24: 21;

        x1 c= the carrier of [:X, Y:];

        then

         A18: x1 c= [:the carrier of X, the carrier of Y:] by BORSUK_1:def 2;

        

         A19: ( dom x1) c= the carrier of X

        proof

          let d be object;

          assume d in ( dom x1);

          then ex e be object st [d, e] in x1 by XTUPLE_0:def 12;

          hence thesis by A18, ZFMISC_1: 87;

        end;

        

        thus ((G * F) . x) = (G . (F . x1)) by A16, A17, FUNCT_1: 12

        .= (G . x1X) by A7

        .= ( *graph x1X) by A3

        .= x by A19, WAYBEL26: 41;

      end;

      then

       A20: (G * F) = ( id ( InclPoset the topology of [:X, Y:])) by A16, FUNCT_1: 17;

      ( ContMaps (X,T)) = ( oContMaps (X,T)) by Th18;

      then F is isomorphic by A6, A8, A15, A20, YELLOW16: 15;

      hence thesis by A7, Def3;

    end;

    

     Lm4: for T be T_0-TopSpace st a4103[T] holds a4104[T]

    proof

      let Y be T_0-TopSpace such that

       A1: a4103[Y];

      let X be Scott TopAugmentation of ( InclPoset the topology of Y);

      reconsider f = ( id X) as continuous Function of X, X;

      

       A2: the RelStr of X = the RelStr of ( InclPoset the topology of Y) by YELLOW_9:def 4;

      ( *graph f) = { [W, y] where W be open Subset of Y, y be Element of Y : y in W }

      proof

        thus ( *graph f) c= { [W, y] where W be open Subset of Y, y be Element of Y : y in W }

        proof

          let a,b be object;

          assume

           A3: [a, b] in ( *graph f);

          then

           A4: a in ( dom f) by WAYBEL26: 38;

          

           A5: b in (f . a) by A3, WAYBEL26: 38;

          ( dom f) = the carrier of ( InclPoset the topology of Y) by A2, FUNCT_2:def 1

          .= the topology of Y by YELLOW_1: 1;

          then

          reconsider a as open Subset of Y by A4, PRE_TOPC:def 2;

          (f . a) = a by A4, FUNCT_1: 18;

          then

          reconsider b as Element of Y by A5;

          b in a by A4, A5, FUNCT_1: 18;

          hence thesis;

        end;

        let e be object;

        assume e in { [W, y] where W be open Subset of Y, y be Element of Y : y in W };

        then

        consider W be open Subset of Y, y be Element of Y such that

         A6: e = [W, y] & y in W;

        W in the topology of Y by PRE_TOPC:def 2;

        then W in the carrier of ( InclPoset the topology of Y) by YELLOW_1: 1;

        then W in ( dom f) & (f . W) = W by A2, FUNCT_1: 18, FUNCT_2:def 1;

        hence thesis by A6, WAYBEL26: 38;

      end;

      hence thesis by A1;

    end;

    

     Lm5: for T be T_0-TopSpace st a4104[T] holds a4105[T]

    proof

      let Y be T_0-TopSpace such that

       A1: a4104[Y];

      let S be Scott TopAugmentation of ( InclPoset the topology of Y);

      reconsider A = { [W, z] where W be open Subset of Y, z be Element of Y : z in W } as open Subset of [:S, Y:] by A1;

      let y be Element of Y, V be open a_neighborhood of y;

      the topology of S is Basis of S & the topology of Y is Basis of Y by CANTOR_1: 2;

      then

      reconsider B = { [:a, b:] where a be Subset of S, b be Subset of Y : a in the topology of S & b in the topology of Y } as Basis of [:S, Y:] by YELLOW_9: 40;

      y in V by CONNSP_2: 4;

      then [V, y] in A;

      then

      consider ab be Subset of [:S, Y:] such that

       A2: ab in B and

       A3: [V, y] in ab and

       A4: ab c= A by YELLOW_9: 31;

      consider H be Subset of S, W be Subset of Y such that

       A5: ab = [:H, W:] and

       A6: H in the topology of S and

       A7: W in the topology of Y by A2;

      reconsider H as open Subset of S by A6, PRE_TOPC:def 2;

      

       A8: the RelStr of S = the RelStr of ( InclPoset the topology of Y) by YELLOW_9:def 4;

      ( meet H) c= the carrier of Y

      proof

        let x be object;

        H <> {} by A3, A5;

        then

        consider A be object such that

         A9: A in H by XBOOLE_0:def 1;

        A in the carrier of S by A9;

        then

         A10: A in the topology of Y by A8, YELLOW_1: 1;

        reconsider A as set by TARSKI: 1;

        assume x in ( meet H);

        then x in A by A9, SETFAM_1:def 1;

        hence thesis by A10;

      end;

      then

      reconsider mH = ( meet H) as Subset of Y;

      reconsider W as open Subset of Y by A7, PRE_TOPC:def 2;

      W c= mH

      proof

        let w be object;

        assume

         A11: w in W;

         A12:

        now

          let a be set;

          assume a in H;

          then [a, w] in ab by A5, A11, ZFMISC_1: 87;

          then [a, w] in A by A4;

          then

          consider a1 be open Subset of Y, w1 be Element of Y such that

           A13: [a, w] = [a1, w1] and

           A14: w1 in a1;

          a = a1 by A13, XTUPLE_0: 1;

          hence w in a by A13, A14, XTUPLE_0: 1;

        end;

        H <> {} by A3, A5;

        hence thesis by A12, SETFAM_1:def 1;

      end;

      then

       A15: W c= ( Int mH) by TOPS_1: 24;

      take H;

      thus V in H by A3, A5, ZFMISC_1: 87;

      y in W by A3, A5, ZFMISC_1: 87;

      hence thesis by A15, CONNSP_2:def 1;

    end;

    

     Lm6: for T be T_0-TopSpace st a4105[T] holds a4103[T]

    proof

      let Y be T_0-TopSpace such that

       A1: a4105[Y];

      let X be non empty TopSpace;

      let T be Scott TopAugmentation of ( InclPoset the topology of Y);

      let f be continuous Function of X, T;

      the topology of X is Basis of X & the topology of Y is Basis of Y by CANTOR_1: 2;

      then

      reconsider B = { [:a, b:] where a be Subset of X, b be Subset of Y : a in the topology of X & b in the topology of Y } as Basis of [:X, Y:] by YELLOW_9: 40;

      

       A2: the RelStr of T = the RelStr of ( InclPoset the topology of Y) by YELLOW_9:def 4;

      now

        let s be object;

        assume

         A3: s in ( *graph f);

        then

        consider s1,s2 be object such that

         A4: s = [s1, s2] by RELAT_1:def 1;

        

         A5: s1 in ( dom f) by A3, A4, WAYBEL26: 38;

        then (f . s1) in ( rng f) by FUNCT_1:def 3;

        then (f . s1) in the carrier of T;

        then

         A6: (f . s1) in the topology of Y by A2, YELLOW_1: 1;

        s2 in (f . s1) by A3, A4, WAYBEL26: 38;

        then s in [:the carrier of X, the carrier of Y:] by A4, A5, A6, ZFMISC_1: 87;

        hence s in the carrier of [:X, Y:] by BORSUK_1:def 2;

      end;

      then

      reconsider A = ( *graph f) as Subset of [:X, Y:] by TARSKI:def 3;

      now

        let p be Point of [:X, Y:];

        assume

         A7: p in A;

        then

        consider x,y be object such that

         A8: p = [x, y] by RELAT_1:def 1;

        

         A9: y in (f . x) by A7, A8, WAYBEL26: 38;

        

         A10: x in ( dom f) by A7, A8, WAYBEL26: 38;

        then

        reconsider x as Element of X;

        (f . x) in the carrier of ( InclPoset the topology of Y) by A2;

        then

         A11: (f . x) in the topology of Y by YELLOW_1: 1;

        then

        reconsider y as Element of Y by A9;

        reconsider W = (f . x) as open Subset of Y by A11, PRE_TOPC:def 2;

        y in ( Int W) by A9, TOPS_1: 23;

        then

        reconsider W as open a_neighborhood of y by CONNSP_2:def 1;

        consider H be open Subset of T such that

         A12: W in H and

         A13: ( meet H) is a_neighborhood of y by A1;

        ( [#] T) <> {} ;

        then

        reconsider fH = (f " H) as open Subset of X by TOPS_2: 43;

        reconsider mH = ( meet H) as a_neighborhood of y by A13;

        ( Int ( Int mH)) = ( Int mH);

        then

        reconsider V = ( Int mH) as open a_neighborhood of y by CONNSP_2:def 1;

        reconsider a = [:fH, V:] as Subset of [:X, Y:];

        take a;

        V in the topology of Y & fH in the topology of X by PRE_TOPC:def 2;

        hence a in B;

        y in ( Int mH) & x in fH by A10, A12, CONNSP_2:def 1, FUNCT_1:def 7;

        hence p in a by A8, ZFMISC_1: 87;

        thus a c= A

        proof

          let s1,s2 be object;

          

           A14: V c= mH by TOPS_1: 16;

          assume

           A15: [s1, s2] in a;

          then

           A16: s1 in fH by ZFMISC_1: 87;

          then

           A17: (f . s1) in H by FUNCT_1:def 7;

          

           A18: s1 in ( dom f) by A16, FUNCT_1:def 7;

          s2 in V by A15, ZFMISC_1: 87;

          then s2 in (f . s1) by A17, A14, SETFAM_1:def 1;

          hence thesis by A18, WAYBEL26: 38;

        end;

      end;

      hence thesis by YELLOW_9: 31;

    end;

    

     Lm7: for T be T_0-TopSpace st a4105[T] holds ( InclPoset the topology of T) is continuous

    proof

      let Y be T_0-TopSpace such that

       A1: a4105[Y];

      set L = ( InclPoset the topology of Y);

      set S = the Scott TopAugmentation of L;

      thus for x be Element of L holds ( waybelow x) is non empty directed;

      thus L is up-complete;

      let A be Element of L;

      the carrier of L = the topology of Y by YELLOW_1: 1;

      then A in the topology of Y;

      then

      reconsider B = A as open Subset of Y by PRE_TOPC:def 2;

      

       A2: the RelStr of S = the RelStr of L by YELLOW_9:def 4;

      thus A c= ( sup ( waybelow A))

      proof

        let x be object;

        assume

         A3: x in A;

        then x in B;

        then

        reconsider x9 = x as Element of Y;

        reconsider B as open a_neighborhood of x9 by A3, CONNSP_2: 3;

        consider H be open Subset of S such that

         A4: B in H and

         A5: ( meet H) is a_neighborhood of x9 by A1;

        reconsider mH = ( meet H) as a_neighborhood of x9 by A5;

        reconsider H1 = H as Subset of L by A2;

        ( Int mH) in the topology of Y by PRE_TOPC:def 2;

        then

        reconsider ImH = ( Int mH) as Element of L by YELLOW_1: 1;

        ImH << A

        proof

          let D be non empty directed Subset of L;

          

           A6: H1 is inaccessible upper by A2, WAYBEL_0: 25, YELLOW_9: 47;

          assume A <= ( sup D);

          then ( sup D) in H1 by A4, A6;

          then D meets H1 by A6;

          then

          consider d be object such that

           A7: d in D and

           A8: d in H1 by XBOOLE_0: 3;

          reconsider d as Element of L by A7;

          take d;

          thus d in D by A7;

          ( Int mH) c= mH & mH c= d by A8, SETFAM_1: 3, TOPS_1: 16;

          then ImH c= d;

          hence thesis by YELLOW_1: 3;

        end;

        then x in ( Int mH) & ( Int mH) in ( waybelow A) by CONNSP_2:def 1;

        then x in ( union ( waybelow A)) by TARSKI:def 4;

        hence thesis by YELLOW_1: 22;

      end;

      ( union ( waybelow A)) c= ( union ( downarrow A)) by WAYBEL_3: 11, ZFMISC_1: 77;

      then ( sup ( waybelow A)) c= ( union ( downarrow A)) by YELLOW_1: 22;

      then ( sup ( waybelow A)) c= ( sup ( downarrow A)) by YELLOW_1: 22;

      hence thesis by WAYBEL_0: 34;

    end;

    

     Lm8: for T be T_0-TopSpace st ( InclPoset the topology of T) is continuous holds a4105[T]

    proof

      let T be T_0-TopSpace;

      assume

       A1: ( InclPoset the topology of T) is continuous;

      let S be Scott TopAugmentation of ( InclPoset the topology of T);

      let y be Element of T, V be open a_neighborhood of y;

      

       A2: ( Int V) c= V & y in ( Int V) by CONNSP_2:def 1, TOPS_1: 16;

      V in the topology of T by PRE_TOPC:def 2;

      then

      reconsider W = V as Element of ( InclPoset the topology of T) by YELLOW_1: 1;

      W = ( sup ( waybelow W)) by A1, WAYBEL_3:def 5

      .= ( union ( waybelow W)) by YELLOW_1: 22;

      then

      consider Z be set such that

       A3: y in Z and

       A4: Z in ( waybelow W) by A2, TARSKI:def 4;

      reconsider Z as Element of ( InclPoset the topology of T) by A4;

      

       A5: the RelStr of ( InclPoset the topology of T) = the RelStr of S by YELLOW_9:def 4;

      then

      reconsider Z1 = Z as Element of S;

      Z in the carrier of ( InclPoset the topology of T);

      then Z in the topology of T by YELLOW_1: 1;

      then

      reconsider Z2 = Z as open Subset of T by PRE_TOPC:def 2;

      

       A6: Z c= ( meet ( uparrow Z))

      proof

        let s be object;

        assume

         A7: s in Z;

        now

          let z be set;

          assume

           A8: z in ( uparrow Z);

          then

          reconsider z1 = z as Element of ( InclPoset the topology of T);

          Z <= z1 by A8, WAYBEL_0: 18;

          then Z c= z by YELLOW_1: 3;

          hence s in z by A7;

        end;

        hence thesis by SETFAM_1:def 1;

      end;

      reconsider H = ( wayabove Z1) as open Subset of S by A1, WAYBEL11: 36;

      take H;

      Z << W by A4, WAYBEL_3: 7;

      then

       A9: V in ( wayabove Z);

      hence

       A10: V in H by A5, YELLOW12: 13;

      ( meet H) c= the carrier of T

      proof

        let s be object;

        assume s in ( meet H);

        then s in V by A10, SETFAM_1:def 1;

        hence thesis;

      end;

      then

      reconsider mH = ( meet H) as Subset of T;

      ( meet ( uparrow Z)) c= ( meet ( wayabove Z)) by A9, SETFAM_1: 6, WAYBEL_3: 11;

      then ( meet ( uparrow Z)) c= ( meet ( wayabove Z1)) by A5, YELLOW12: 13;

      then Z2 c= mH by A6;

      then Z2 c= ( Int mH) by TOPS_1: 24;

      hence thesis by A3, CONNSP_2:def 1;

    end;

    begin

    theorem :: WAYBEL29:24

    for Y be T_0-TopSpace holds (for X be non empty TopSpace holds for L be Scott continuous complete TopLattice holds for T be Scott TopAugmentation of ( ContMaps (Y,L)) holds ex f be Function of ( ContMaps (X,T)), ( ContMaps ( [:X, Y:],L)), g be Function of ( ContMaps ( [:X, Y:],L)), ( ContMaps (X,T)) st f is uncurrying one-to-one onto & g is currying one-to-one onto) iff for X be non empty TopSpace holds for L be Scott continuous complete TopLattice holds for T be Scott TopAugmentation of ( ContMaps (Y,L)) holds ex f be Function of ( ContMaps (X,T)), ( ContMaps ( [:X, Y:],L)), g be Function of ( ContMaps ( [:X, Y:],L)), ( ContMaps (X,T)) st f is uncurrying isomorphic & g is currying isomorphic by Lm1;

    theorem :: WAYBEL29:25

    for Y be T_0-TopSpace holds ( InclPoset the topology of Y) is continuous iff for X be non empty TopSpace holds ( Theta (X,Y)) is isomorphic

    proof

      let Y be T_0-TopSpace;

      hereby

        assume ( InclPoset the topology of Y) is continuous;

        then a4105[Y] by Lm8;

        then a4103[Y] by Lm6;

        hence a4102[Y] by Lm3;

      end;

      assume a4102[Y];

      then a4103[Y] by Lm2;

      then a4104[Y] by Lm4;

      then a4105[Y] by Lm5;

      hence thesis by Lm7;

    end;

    theorem :: WAYBEL29:26

    for Y be T_0-TopSpace holds ( InclPoset the topology of Y) is continuous iff for X be non empty TopSpace holds for f be continuous Function of X, ( Sigma ( InclPoset the topology of Y)) holds ( *graph f) is open Subset of [:X, Y:]

    proof

      let Y be T_0-TopSpace;

      hereby

        assume ( InclPoset the topology of Y) is continuous;

        then a4105[Y] by Lm8;

        hence for X be non empty TopSpace holds for f be continuous Function of X, ( Sigma ( InclPoset the topology of Y)) holds ( *graph f) is open Subset of [:X, Y:] by Lm6;

      end;

      assume

       A1: for X be non empty TopSpace holds for f be continuous Function of X, ( Sigma ( InclPoset the topology of Y)) holds ( *graph f) is open Subset of [:X, Y:];

       a4103[Y]

      proof

        let X be non empty TopSpace;

        let T be Scott TopAugmentation of ( InclPoset the topology of Y);

        let f be continuous Function of X, T;

        

         A2: the RelStr of T = ( InclPoset the topology of Y) & the RelStr of ( Sigma ( InclPoset the topology of Y)) = ( InclPoset the topology of Y) by YELLOW_9:def 4;

        then

        reconsider g = f as Function of X, ( Sigma ( InclPoset the topology of Y));

         the TopStruct of X = the TopStruct of X & the TopStruct of T = the TopStruct of ( Sigma ( InclPoset the topology of Y)) by A2, Th13;

        then g is continuous by YELLOW12: 36;

        hence thesis by A1;

      end;

      then a4104[Y] by Lm4;

      then a4105[Y] by Lm5;

      hence thesis by Lm7;

    end;

    theorem :: WAYBEL29:27

    for Y be T_0-TopSpace holds ( InclPoset the topology of Y) is continuous iff { [W, y] where W be open Subset of Y, y be Element of Y : y in W } is open Subset of [:( Sigma ( InclPoset the topology of Y)), Y:]

    proof

      let Y be T_0-TopSpace;

      hereby

        assume ( InclPoset the topology of Y) is continuous;

        then a4105[Y] by Lm8;

        then a4103[Y] by Lm6;

        hence { [W, y] where W be open Subset of Y, y be Element of Y : y in W } is open Subset of [:( Sigma ( InclPoset the topology of Y)), Y:] by Lm4;

      end;

      assume

       A1: { [W, y] where W be open Subset of Y, y be Element of Y : y in W } is open Subset of [:( Sigma ( InclPoset the topology of Y)), Y:];

       a4104[Y]

      proof

        let T be Scott TopAugmentation of ( InclPoset the topology of Y);

         the RelStr of T = ( InclPoset the topology of Y) & the RelStr of ( Sigma ( InclPoset the topology of Y)) = ( InclPoset the topology of Y) by YELLOW_9:def 4;

        then the TopStruct of Y = the TopStruct of Y & the TopStruct of T = the TopStruct of ( Sigma ( InclPoset the topology of Y)) by Th13;

        then [:T, Y:] = [:( Sigma ( InclPoset the topology of Y)), Y:] by Th7;

        hence thesis by A1;

      end;

      then a4105[Y] by Lm5;

      hence thesis by Lm7;

    end;

    theorem :: WAYBEL29:28

    for Y be T_0-TopSpace holds ( InclPoset the topology of Y) is continuous iff for y be Element of Y, V be open a_neighborhood of y holds ex H be open Subset of ( Sigma ( InclPoset the topology of Y)) st V in H & ( meet H) is a_neighborhood of y

    proof

      let Y be T_0-TopSpace;

      thus ( InclPoset the topology of Y) is continuous implies for y be Element of Y, V be open a_neighborhood of y holds ex H be open Subset of ( Sigma ( InclPoset the topology of Y)) st V in H & ( meet H) is a_neighborhood of y by Lm8;

      assume

       A1: for y be Element of Y, V be open a_neighborhood of y holds ex H be open Subset of ( Sigma ( InclPoset the topology of Y)) st V in H & ( meet H) is a_neighborhood of y;

       a4105[Y]

      proof

        let T be Scott TopAugmentation of ( InclPoset the topology of Y);

        let y be Element of Y, V be open a_neighborhood of y;

        consider H be open Subset of ( Sigma ( InclPoset the topology of Y)) such that

         A2: V in H & ( meet H) is a_neighborhood of y by A1;

         the RelStr of T = ( InclPoset the topology of Y) & the RelStr of ( Sigma ( InclPoset the topology of Y)) = ( InclPoset the topology of Y) by YELLOW_9:def 4;

        then

        reconsider G = H as Subset of T;

        the topology of T = the topology of ( Sigma ( InclPoset the topology of Y)) by Th13;

        then G in the topology of T by PRE_TOPC:def 2;

        then H is open Subset of T by PRE_TOPC:def 2;

        hence thesis by A2;

      end;

      hence thesis by Lm7;

    end;

    defpred a4111[ complete LATTICE] means ( InclPoset ( sigma $1)) is continuous;

    defpred a4112[ complete LATTICE] means for SL be Scott TopAugmentation of $1 holds for S be complete LATTICE holds for SS be Scott TopAugmentation of S holds ( sigma [:S, $1:]) = the topology of [:SS, SL:];

    defpred a4113[ complete LATTICE] means for SL be Scott TopAugmentation of $1 holds for S be complete LATTICE holds for SS be Scott TopAugmentation of S holds for SSL be Scott TopAugmentation of [:S, $1:] holds the TopStruct of SSL = [:SS, SL:];

    

     Lm9: for L be complete LATTICE holds a4112[L] iff a4113[L]

    proof

      let L be complete LATTICE;

      thus a4112[L] implies a4113[L]

      proof

        assume

         A1: a4112[L];

        let SL be Scott TopAugmentation of L;

        let S be complete LATTICE;

        let SS be Scott TopAugmentation of S;

        let SSL be Scott TopAugmentation of [:S, L:];

        

         A2: the topology of [:SS, SL:] = ( sigma [:S, L:]) by A1

        .= the topology of SSL by YELLOW_9: 51;

        

         A3: the RelStr of SSL = the RelStr of [:S, L:] by YELLOW_9:def 4;

         the RelStr of SL = the RelStr of L & the RelStr of SS = the RelStr of S by YELLOW_9:def 4;

        

        then the carrier of SSL = [:the carrier of SS, the carrier of SL:] by A3, YELLOW_3:def 2

        .= the carrier of [:SS, SL:] by BORSUK_1:def 2;

        hence thesis by A2;

      end;

      assume

       A4: a4113[L];

      let SL be Scott TopAugmentation of L;

      let S be complete LATTICE;

      let SS be Scott TopAugmentation of S;

      now

        let SSL be Scott TopAugmentation of [:S, L:];

         the TopStruct of SSL = the TopStruct of [:SS, SL:] by A4;

        hence thesis by YELLOW_9: 51;

      end;

      hence thesis;

    end;

    begin

    theorem :: WAYBEL29:29

    for R1,R2,R3 be non empty RelStr holds for f1 be Function of R1, R3 st f1 is isomorphic holds for f2 be Function of R2, R3 st f2 = f1 & f2 is isomorphic holds the RelStr of R1 = the RelStr of R2

    proof

      let R1,R2,R3 be non empty RelStr;

      let f1 be Function of R1, R3;

      assume

       A1: f1 is isomorphic;

      let f2 be Function of R2, R3;

      assume that

       A2: f2 = f1 and

       A3: f2 is isomorphic;

      

       A4: the carrier of R1 = ( rng (f2 qua Function " )) by A1, A2, WAYBEL_0: 67

      .= the carrier of R2 by A3, WAYBEL_0: 67;

      

       A5: the InternalRel of R2 c= the InternalRel of R1

      proof

        let x1,x2 be object;

        assume

         A6: [x1, x2] in the InternalRel of R2;

        then

        reconsider x19 = x1, x29 = x2 as Element of R2 by ZFMISC_1: 87;

        reconsider y1 = x19, y2 = x29 as Element of R1 by A4;

        x19 <= x29 by A6, ORDERS_2:def 5;

        then (f2 . x19) <= (f2 . x29) by A3, WAYBEL_0: 66;

        then y1 <= y2 by A1, A2, WAYBEL_0: 66;

        hence thesis by ORDERS_2:def 5;

      end;

      the InternalRel of R1 c= the InternalRel of R2

      proof

        let x1,x2 be object;

        assume

         A7: [x1, x2] in the InternalRel of R1;

        then

        reconsider x19 = x1, x29 = x2 as Element of R1 by ZFMISC_1: 87;

        reconsider y1 = x19, y2 = x29 as Element of R2 by A4;

        x19 <= x29 by A7, ORDERS_2:def 5;

        then (f1 . x19) <= (f1 . x29) by A1, WAYBEL_0: 66;

        then y1 <= y2 by A2, A3, WAYBEL_0: 66;

        hence thesis by ORDERS_2:def 5;

      end;

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

    end;

    

     Lm10: for L be complete LATTICE holds a4111[L] implies a4112[L]

    proof

      let L be complete LATTICE;

      assume

       A1: a4111[L];

      let SL be Scott TopAugmentation of L;

      let S be complete LATTICE;

      let SS be Scott TopAugmentation of S;

      

       A2: the RelStr of SS = the RelStr of S by YELLOW_9:def 4;

      ( UPS (L,( BoolePoset { 0 }))) is non empty full SubRelStr of (( BoolePoset { 0 }) |^ the carrier of L) by WAYBEL27:def 4;

      then

       A3: (( UPS (L,( BoolePoset { 0 }))) |^ the carrier of S) is non empty full SubRelStr of ((( BoolePoset { 0 }) |^ the carrier of L) |^ the carrier of S) by YELLOW16: 39;

      ( UPS (S,( UPS (L,( BoolePoset { 0 }))))) is non empty full SubRelStr of (( UPS (L,( BoolePoset { 0 }))) |^ the carrier of S) by WAYBEL27:def 4;

      then

       A4: ( UPS (S,( UPS (L,( BoolePoset { 0 }))))) is non empty full SubRelStr of ((( BoolePoset { 0 }) |^ the carrier of L) |^ the carrier of S) by A3, WAYBEL15: 1;

      consider f5 be Function of ( UPS (L,( BoolePoset { 0 }))), ( InclPoset ( sigma L)) such that

       A5: f5 is isomorphic and

       A6: for f be directed-sups-preserving Function of L, ( BoolePoset { 0 }) holds (f5 . f) = (f " {1}) by WAYBEL27: 33;

      set f6 = ( UPS (( id S),f5));

      consider f3 be Function of ( UPS (S,( UPS (L,( BoolePoset { 0 }))))), ( UPS ( [:S, L:],( BoolePoset { 0 }))) such that

       A7: f3 is uncurrying isomorphic by WAYBEL27: 47;

      set f4 = (f3 " );

      set T = ( Sigma ( InclPoset the topology of SL));

      consider f1 be Function of ( UPS ( [:S, L:],( BoolePoset { 0 }))), ( InclPoset ( sigma [:S, L:])) such that

       A8: f1 is isomorphic and

       A9: for f be directed-sups-preserving Function of [:S, L:], ( BoolePoset { 0 }) holds (f1 . f) = (f " {1}) by WAYBEL27: 33;

      

       A10: f4 is isomorphic by A7, YELLOW14: 10;

      set f2 = (f1 " );

      set G = ((f6 * f4) * f2);

      

       A11: the topology of SL = ( sigma L) by YELLOW_9: 51;

      then

       A12: the RelStr of T = the RelStr of ( InclPoset ( sigma L)) by YELLOW_9:def 4;

      

       A13: the carrier of ( UPS (S,( InclPoset ( sigma L)))) = the carrier of ( ContMaps (SS,T))

      proof

        thus the carrier of ( UPS (S,( InclPoset ( sigma L)))) c= the carrier of ( ContMaps (SS,T))

        proof

          let x be object;

          assume

           A14: x in the carrier of ( UPS (S,( InclPoset ( sigma L))));

          then

          reconsider x1 = x as Function of SS, T by A2, A12, WAYBEL27:def 4;

          x is directed-sups-preserving Function of S, ( InclPoset ( sigma L)) by A14, WAYBEL27:def 4;

          then x1 is directed-sups-preserving by A2, A12, WAYBEL21: 6;

          then x1 is continuous by WAYBEL17: 22;

          hence thesis by WAYBEL24:def 3;

        end;

        let x be object;

        assume x in the carrier of ( ContMaps (SS,T));

        then

        consider x1 be Function of SS, T such that

         A15: x1 = x and

         A16: x1 is continuous by WAYBEL24:def 3;

        reconsider x2 = x1 as Function of S, ( InclPoset ( sigma L)) by A2, A12;

        x1 is directed-sups-preserving by A16, WAYBEL17: 22;

        then x2 is directed-sups-preserving by A2, A12, WAYBEL21: 6;

        hence thesis by A15, WAYBEL27:def 4;

      end;

      then

      reconsider G as Function of ( InclPoset ( sigma [:S, L:])), ( ContMaps (SS,T));

      set F = ( Theta (SS,SL));

      

       A17: the RelStr of SL = the RelStr of L by YELLOW_9:def 4;

      (( BoolePoset { 0 }) |^ the carrier of [:S, L:]) = (( BoolePoset { 0 }) |^ [:the carrier of S, the carrier of L:]) & ( UPS ( [:S, L:],( BoolePoset { 0 }))) is non empty full SubRelStr of (( BoolePoset { 0 }) |^ the carrier of [:S, L:]) by WAYBEL27:def 4, YELLOW_3:def 2;

      then

       A18: f4 is currying by A7, A4, Th2;

      

       A19: for V be Element of ( InclPoset ( sigma [:S, L:])) holds for s be Element of S holds ((G . V) . s) = { y where y be Element of L : [s, y] in V }

      proof

        let V be Element of ( InclPoset ( sigma [:S, L:]));

        let s be Element of S;

        reconsider fff = (f4 . (f2 . V)) as directed-sups-preserving Function of S, ( UPS (L,( BoolePoset { 0 }))) by WAYBEL27:def 4;

        reconsider f2V = (f2 . V) as directed-sups-preserving Function of [:S, L:], ( BoolePoset { 0 }) by WAYBEL27:def 4;

        

         A20: f5 is sups-preserving & ((f5 * fff) * ( id the carrier of S)) = (f5 * fff) by A5, FUNCT_2: 17, WAYBEL13: 20;

        

         A21: ((f4 . (f2 . V)) . s) is directed-sups-preserving Function of L, ( BoolePoset { 0 }) by WAYBEL27:def 4;

        then

         A22: ( dom ((f4 . (f2 . V)) . s)) = the carrier of L by FUNCT_2:def 1;

        (G . V) = ((f6 * f4) . (f2 . V)) by FUNCT_2: 15

        .= (( UPS (( id S),f5)) . (f4 . (f2 . V))) by FUNCT_2: 15

        .= (f5 * fff) by A20, WAYBEL27:def 5;

        

        then

         A23: ((G . V) . s) = (f5 . (fff . s)) by FUNCT_2: 15

        .= (((f4 . (f2 . V)) . s) " {1}) by A6, A21;

        

         A24: ( rng f1) = ( [#] ( InclPoset ( sigma [:S, L:]))) by A8, FUNCT_2:def 3;

        ( dom f4) = the carrier of ( UPS ( [:S, L:],( BoolePoset { 0 }))) by FUNCT_2:def 1;

        then

         A25: (f4 . (f2 . V)) = ( curry (f2 . V)) by A18;

        ( rng f1) = the carrier of ( InclPoset ( sigma [:S, L:])) by A8, FUNCT_2:def 3;

        

        then

         A26: V = (( id ( rng f1)) . V)

        .= ((f1 * f2) . V) by A8, A24, TOPS_2: 52

        .= (f1 . (f2 . V)) by FUNCT_2: 15

        .= (f2V " {1}) by A9;

        thus ((G . V) . s) c= { y where y be Element of L : [s, y] in V }

        proof

          let x be object;

          assume

           A27: x in ((G . V) . s);

          then x in ( dom ((f4 . (f2 . V)) . s)) by A23, FUNCT_1:def 7;

          then

          reconsider y = x as Element of L by A21, FUNCT_2:def 1;

          (((f4 . (f2 . V)) . s) . x) in {1} by A23, A27, FUNCT_1:def 7;

          then

           A28: (((f4 . (f2 . V)) . s) . y) = 1 by TARSKI:def 1;

          

           A29: ( dom f2V) = the carrier of [:S, L:] by FUNCT_2:def 1;

          then [s, y] in ( dom (f2 . V));

          then ((f2 . V) . (s,y)) = 1 by A25, A28, FUNCT_5: 20;

          then ((f2 . V) . (s,y)) in {1} by TARSKI:def 1;

          then [s, y] in ((f2 . V) " {1}) by A29, FUNCT_1:def 7;

          hence thesis by A26;

        end;

        let x be object;

        assume x in { y where y be Element of L : [s, y] in V };

        then

        consider y be Element of L such that

         A30: y = x and

         A31: [s, y] in V;

        ( dom f2V) = the carrier of [:S, L:] by FUNCT_2:def 1;

        then

         A32: [s, y] in ( dom (f2 . V));

        reconsider cs = (( curry (f2 . V)) . s) as Function;

        ((f2 . V) . (s,y)) in {1} by A26, A31, FUNCT_1:def 7;

        then ((f2 . V) . (s,y)) = 1 by TARSKI:def 1;

        then (cs . y) = 1 by A32, FUNCT_5: 20;

        then (((f4 . (f2 . V)) . s) . y) in {1} by A25, TARSKI:def 1;

        hence thesis by A23, A30, A22, FUNCT_1:def 7;

      end;

       a4105[SL] by A1, A11, Lm8;

      then a4103[SL] by Lm6;

      then

       A33: F is isomorphic by Lm3;

      

       A34: the carrier of ( InclPoset ( sigma [:S, L:])) c= the carrier of ( InclPoset the topology of [:SS, SL:])

      proof

        let V be object;

        assume V in the carrier of ( InclPoset ( sigma [:S, L:]));

        then

        reconsider V1 = V as Element of ( InclPoset ( sigma [:S, L:]));

        ( rng F) = the carrier of ( ContMaps (SS,T)) by A33, FUNCT_2:def 3;

        then

        consider W be object such that

         A35: W in ( dom F) and

         A36: (F . W) = (G . V1) by FUNCT_1:def 3;

        reconsider W2 = W as Element of ( InclPoset the topology of [:SS, SL:]) by A35;

        ( dom F) = the carrier of ( InclPoset the topology of [:SS, SL:]) by FUNCT_2:def 1;

        then W in the topology of [:SS, SL:] by A35, YELLOW_1: 1;

        then

        reconsider W1 = W2 as open Subset of [:SS, SL:] by PRE_TOPC:def 2;

        

         A37: V1 c= W1

        proof

          let v be object;

          assume

           A38: v in V1;

          V1 in the carrier of ( InclPoset ( sigma [:S, L:]));

          then V in ( sigma [:S, L:]) by YELLOW_1: 1;

          then V1 c= the carrier of [:S, L:];

          then V1 c= [:the carrier of S, the carrier of L:] by YELLOW_3:def 2;

          then

          consider v1,v2 be object such that

           A39: v1 in the carrier of S and

           A40: v2 in the carrier of L and

           A41: v = [v1, v2] by A38, ZFMISC_1: 84;

          reconsider v2 as Element of L by A40;

          reconsider v1 as Element of S by A39;

          v2 in { y where y be Element of L : [v1, y] in V1 } by A38, A41;

          then v2 in ((G . V1) . v1) by A19;

          then v2 in (((W1,the carrier of S) *graph ) . v1) by A2, A36, Def3;

          then v2 in ( Im (W1,v1)) by WAYBEL26:def 5;

          then ex v19 be object st [v19, v2] in W1 & v19 in {v1} by RELAT_1:def 13;

          hence thesis by A41, TARSKI:def 1;

        end;

        W2 c= V1

        proof

          let w be object;

          assume

           A42: w in W2;

          W1 c= the carrier of [:SS, SL:];

          then W1 c= [:the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;

          then

          consider w1,w2 be object such that

           A43: w1 in the carrier of S and

           A44: w2 in the carrier of L and

           A45: w = [w1, w2] by A2, A17, A42, ZFMISC_1: 84;

          reconsider w2 as Element of L by A44;

          reconsider w1 as Element of S by A43;

          w1 in {w1} by TARSKI:def 1;

          then w2 in ( Im (W1,w1)) by A42, A45, RELAT_1:def 13;

          then w2 in (((W1,the carrier of S) *graph ) . w1) by WAYBEL26:def 5;

          then w2 in ((F . W2) . w1) by A2, Def3;

          then w2 in { y where y be Element of L : [w1, y] in V1 } by A19, A36;

          then ex w29 be Element of L st w29 = w2 & [w1, w29] in V1;

          hence thesis by A45;

        end;

        then W2 = V by A37, XBOOLE_0:def 10;

        hence thesis;

      end;

      ( InclPoset ( sigma L)) = ( InclPoset the topology of SL) by YELLOW_9: 51;

      then f6 is isomorphic by A5, WAYBEL27: 35;

      then

       A46: (f6 * f4) is isomorphic by A10, Th6;

      

       A47: f2 is isomorphic by A8, YELLOW14: 10;

      the carrier of ( InclPoset the topology of [:SS, SL:]) c= the carrier of ( InclPoset ( sigma [:S, L:]))

      proof

        let W be object;

        assume

         A48: W in the carrier of ( InclPoset the topology of [:SS, SL:]);

        then

        reconsider W2 = W as Element of ( InclPoset the topology of [:SS, SL:]);

        W in the topology of [:SS, SL:] by A48, YELLOW_1: 1;

        then

        reconsider W1 = W2 as open Subset of [:SS, SL:] by PRE_TOPC:def 2;

        G is onto by A47, A46, A13, Th6, YELLOW14: 9;

        then ( rng G) = the carrier of ( ContMaps (SS,T)) by FUNCT_2:def 3;

        then

        consider V be object such that

         A49: V in ( dom G) and

         A50: (G . V) = (F . W2) by FUNCT_1:def 3;

        reconsider V as Element of ( InclPoset ( sigma [:S, L:])) by A49;

        

         A51: V c= W2

        proof

          let v be object;

          assume

           A52: v in V;

          V in the carrier of ( InclPoset ( sigma [:S, L:]));

          then V in ( sigma [:S, L:]) by YELLOW_1: 1;

          then V c= the carrier of [:S, L:];

          then V c= [:the carrier of S, the carrier of L:] by YELLOW_3:def 2;

          then

          consider v1,v2 be object such that

           A53: v1 in the carrier of S and

           A54: v2 in the carrier of L and

           A55: v = [v1, v2] by A52, ZFMISC_1: 84;

          reconsider v2 as Element of L by A54;

          reconsider v1 as Element of S by A53;

          v2 in { y where y be Element of L : [v1, y] in V } by A52, A55;

          then v2 in ((G . V) . v1) by A19;

          then v2 in (((W1,the carrier of S) *graph ) . v1) by A2, A50, Def3;

          then v2 in ( Im (W1,v1)) by WAYBEL26:def 5;

          then ex v19 be object st [v19, v2] in W2 & v19 in {v1} by RELAT_1:def 13;

          hence thesis by A55, TARSKI:def 1;

        end;

        W2 c= V

        proof

          let w be object;

          assume

           A56: w in W2;

          W1 c= the carrier of [:SS, SL:];

          then W1 c= [:the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;

          then

          consider w1,w2 be object such that

           A57: w1 in the carrier of S and

           A58: w2 in the carrier of L and

           A59: w = [w1, w2] by A2, A17, A56, ZFMISC_1: 84;

          reconsider w2 as Element of L by A58;

          reconsider w1 as Element of S by A57;

          w1 in {w1} by TARSKI:def 1;

          then w2 in ( Im (W1,w1)) by A56, A59, RELAT_1:def 13;

          then w2 in (((W1,the carrier of S) *graph ) . w1) by WAYBEL26:def 5;

          then w2 in ((F . W2) . w1) by A2, Def3;

          then w2 in { y where y be Element of L : [w1, y] in V } by A19, A50;

          then ex w29 be Element of L st w29 = w2 & [w1, w29] in V;

          hence thesis by A59;

        end;

        then W = V by A51, XBOOLE_0:def 10;

        hence thesis;

      end;

      then the carrier of ( InclPoset ( sigma [:S, L:])) = the carrier of ( InclPoset the topology of [:SS, SL:]) by A34;

      

      hence ( sigma [:S, L:]) = the carrier of ( InclPoset the topology of [:SS, SL:]) by YELLOW_1: 1

      .= the topology of [:SS, SL:] by YELLOW_1: 1;

    end;

    

     Lm11: for L be complete LATTICE holds a4112[L] implies a4111[L]

    proof

      let L be complete LATTICE;

      set SL = the Scott TopAugmentation of L;

      

       A1: the RelStr of SL = the RelStr of L by YELLOW_9:def 4;

       the TopStruct of SL = ( ConvergenceSpace ( Scott-Convergence SL)) by WAYBEL11: 32;

      then

       A2: the topology of SL = ( sigma SL);

      then

       A3: ( InclPoset ( sigma L)) = ( InclPoset the topology of SL) by A1, YELLOW_9: 52;

      then

      reconsider S = ( InclPoset ( sigma L)) as complete LATTICE;

      set SS = the Scott TopAugmentation of S;

      assume a4112[L];

      then

       A4: ( sigma [:S, L:]) = the topology of [:SS, SL:];

      

       A5: a4104[SL]

      proof

        set Wy = { [W, y] where W be open Subset of SL, y be Element of SL : y in W };

        let T be Scott TopAugmentation of ( InclPoset the topology of SL);

        Wy c= the carrier of [:T, SL:]

        proof

          let x be object;

          

           A6: the RelStr of T = the RelStr of ( InclPoset the topology of SL) by YELLOW_9:def 4;

          assume x in Wy;

          then

          consider W be open Subset of SL, y be Element of SL such that

           A7: x = [W, y] and y in W;

          W in the topology of SL by PRE_TOPC:def 2;

          then W in the carrier of ( InclPoset the topology of SL) by YELLOW_1: 1;

          then [W, y] in [:the carrier of T, the carrier of SL:] by A6, ZFMISC_1: 87;

          hence thesis by A7, BORSUK_1:def 2;

        end;

        then

        reconsider WY = Wy as Subset of [:T, SL:];

        

         A8: the RelStr of SS = the RelStr of ( InclPoset the topology of SL) by A3, YELLOW_9:def 4

        .= the RelStr of T by YELLOW_9:def 4;

        reconsider T1 = T as Scott TopAugmentation of S by A1, A2, YELLOW_9: 52;

        

         A9: the RelStr of SS = the RelStr of S by YELLOW_9:def 4;

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

        .= the carrier of [:S, L:] by A1, A8, A9, YELLOW_3:def 2;

        then

        reconsider wy = WY as Subset of [:S, L:];

        

         A10: wy is inaccessible

        proof

          let D be non empty directed Subset of [:S, L:];

          assume ( sup D) in wy;

          then [( sup ( proj1 D)), ( sup ( proj2 D))] in wy by YELLOW_3: 46;

          then

          consider sp1D be open Subset of SL, sp2D be Element of SL such that

           A11: [( sup ( proj1 D)), ( sup ( proj2 D))] = [sp1D, sp2D] and

           A12: sp2D in sp1D;

          reconsider sp1D9 = sp1D as Subset of L by A1;

          reconsider sp1D9 as inaccessible upper Subset of L by A1, WAYBEL_0: 25, YELLOW_9: 47;

          reconsider pD = ( proj1 D) as Subset of ( InclPoset the topology of SL) by A1, A2, YELLOW_9: 52;

          reconsider proj2D = ( proj2 D) as directed non empty Subset of L by YELLOW_3: 21, YELLOW_3: 22;

          

           A13: ( sup ( proj1 D)) = ( union pD) by A3, YELLOW_1: 22;

          ( sup proj2D) in sp1D9 by A11, A12, XTUPLE_0: 1;

          then ( proj2 D) meets sp1D by WAYBEL11:def 1;

          then

          consider d be object such that

           A14: d in ( proj2 D) and

           A15: d in sp1D by XBOOLE_0: 3;

          reconsider d as Element of L by A14;

          d in ( sup ( proj1 D)) by A11, A15, XTUPLE_0: 1;

          then

          consider V be set such that

           A16: d in V and

           A17: V in ( proj1 D) by A13, TARSKI:def 4;

          consider Y be object such that

           A18: [Y, d] in D by A14, XTUPLE_0:def 13;

          reconsider V as Element of S by A17;

          consider e be object such that

           A19: [V, e] in D by A17, XTUPLE_0:def 12;

          

           A20: Y in ( proj1 D) by A18, XTUPLE_0:def 12;

          

           A21: e in ( proj2 D) by A19, XTUPLE_0:def 13;

          reconsider Y as Element of S by A20;

          reconsider e as Element of L by A21;

          consider DD be Element of [:S, L:] such that

           A22: DD in D and

           A23: [V, e] <= DD and

           A24: [Y, d] <= DD by A18, A19, WAYBEL_0:def 1;

          D c= the carrier of [:S, L:];

          then D c= [:the carrier of S, the carrier of L:] by YELLOW_3:def 2;

          then

          consider DD1,DD2 be object such that

           A25: DD = [DD1, DD2] by A22, RELAT_1:def 1;

          

           A26: DD2 in ( proj2 D) by A22, A25, XTUPLE_0:def 13;

          

           A27: DD1 in ( proj1 D) by A22, A25, XTUPLE_0:def 12;

          reconsider DD2 as Element of L by A26;

          reconsider DD1 as Element of S by A27;

           [V, e] <= [DD1, DD2] by A23, A25;

          then V <= DD1 by YELLOW_3: 11;

          then

           A28: V c= DD1 by YELLOW_1: 3;

          DD1 in the carrier of S;

          then DD1 in ( sigma L) by YELLOW_1: 1;

          then DD1 in the topology of SL by A1, A2, YELLOW_9: 52;

          then DD1 is open Subset of SL by PRE_TOPC:def 2;

          then

           A29: DD1 is upper Subset of L by A1, WAYBEL_0: 25;

           [Y, d] <= [DD1, DD2] by A24, A25;

          then d <= DD2 by YELLOW_3: 11;

          then

           A30: DD2 in DD1 by A16, A28, A29, WAYBEL_0:def 20;

          DD1 in the carrier of S;

          then DD1 in ( sigma L) by YELLOW_1: 1;

          then DD1 in the topology of SL by A1, A2, YELLOW_9: 52;

          then

          reconsider DD1 as open Subset of SL by PRE_TOPC:def 2;

          reconsider DD2 as Element of SL by A1;

           [DD1, DD2] in wy by A30;

          hence thesis by A22, A25, XBOOLE_0: 3;

        end;

        wy is upper

        proof

          let x,y be Element of [:S, L:];

          assume that

           A31: x in wy and

           A32: x <= y;

          consider x1 be open Subset of SL, x2 be Element of SL such that

           A33: x = [x1, x2] and

           A34: x2 in x1 by A31;

          reconsider u2 = x2 as Element of L by A1;

          x1 in the topology of SL by PRE_TOPC:def 2;

          then x1 in ( sigma L) by A1, A2, YELLOW_9: 52;

          then

          reconsider u1 = x1 as Element of S by YELLOW_1: 1;

          the carrier of [:S, L:] = [:the carrier of S, the carrier of L:] by YELLOW_3:def 2;

          then

          consider y1,y2 be object such that

           A35: y1 in the carrier of S and

           A36: y2 in the carrier of L and

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

          y1 in ( sigma L) by A35, YELLOW_1: 1;

          then y1 in the topology of SL by A1, A2, YELLOW_9: 52;

          then

          reconsider y1 as open Subset of SL by PRE_TOPC:def 2;

          reconsider y2 as Element of SL by A1, A36;

          reconsider v2 = y2 as Element of L by A36;

          y1 in the topology of SL by PRE_TOPC:def 2;

          then y1 in ( sigma L) by A1, A2, YELLOW_9: 52;

          then

          reconsider v1 = y1 as Element of S by YELLOW_1: 1;

          

           A38: [u1, u2] <= [v1, v2] by A32, A37, A33;

          then u2 <= v2 by YELLOW_3: 11;

          then x2 <= y2 by A1, YELLOW_0: 1;

          then

           A39: y2 in x1 by A34, WAYBEL_0:def 20;

          u1 <= v1 by A38, YELLOW_3: 11;

          then x1 c= y1 by YELLOW_1: 3;

          hence thesis by A37, A39;

        end;

        then

         A40: wy in the topology of ( ConvergenceSpace ( Scott-Convergence [:S, L:])) by A10, WAYBEL11: 31;

        the topology of SS = ( sigma S) by YELLOW_9: 51

        .= the topology of T1 by YELLOW_9: 51

        .= the topology of T;

        then

         A41: the TopStruct of SS = the TopStruct of T by A8;

         the TopStruct of SL = the TopStruct of SL;

        then [:SS, SL:] = [:T, SL:] by A41, Th7;

        hence thesis by A4, A40, PRE_TOPC:def 2;

      end;

       a4104[SL] implies ( InclPoset the topology of SL) is continuous

      proof

        assume a4104[SL];

        then a4105[SL] by Lm5;

        hence thesis by Lm7;

      end;

      hence thesis by A1, A2, A5, YELLOW_9: 52;

    end;

    theorem :: WAYBEL29:30

    

     Th30: for L be complete LATTICE holds ( InclPoset ( sigma L)) is continuous iff for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):]

    proof

      let L be complete LATTICE;

      thus ( InclPoset ( sigma L)) is continuous implies for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):] by Lm10;

      assume

       A1: for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):];

      now

        let SL be Scott TopAugmentation of L;

        let S be complete LATTICE, SS be Scott TopAugmentation of S;

         the RelStr of SL = the RelStr of L & the RelStr of ( Sigma L) = the RelStr of L by YELLOW_9:def 4;

        then

         A2: the TopStruct of ( Sigma L) = the TopStruct of SL by Th13;

         the RelStr of SS = the RelStr of S & the RelStr of ( Sigma S) = the RelStr of S by YELLOW_9:def 4;

        then the TopStruct of ( Sigma S) = the TopStruct of SS by Th13;

        then [:SS, SL:] = [:( Sigma S), ( Sigma L):] by A2, Th7;

        hence ( sigma [:S, L:]) = the topology of [:SS, SL:] by A1;

      end;

      hence thesis by Lm11;

    end;

    theorem :: WAYBEL29:31

    

     Th31: for L be complete LATTICE holds (for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):]) iff for S be complete LATTICE holds the TopStruct of ( Sigma [:S, L:]) = [:( Sigma S), ( Sigma L):]

    proof

      let L be complete LATTICE;

      hereby

        assume

         A1: for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):];

         a4112[L]

        proof

          let SL be Scott TopAugmentation of L;

          let S be complete LATTICE;

          let SS be Scott TopAugmentation of S;

           the RelStr of SL = the RelStr of L & the RelStr of ( Sigma L) = the RelStr of L by YELLOW_9:def 4;

          then

           A2: the TopStruct of ( Sigma L) = the TopStruct of SL by Th13;

           the RelStr of SS = the RelStr of S & the RelStr of ( Sigma S) = the RelStr of S by YELLOW_9:def 4;

          then the TopStruct of ( Sigma S) = the TopStruct of SS by Th13;

          then [:SS, SL:] = [:( Sigma S), ( Sigma L):] by A2, Th7;

          hence thesis by A1;

        end;

        hence for S be complete LATTICE holds the TopStruct of ( Sigma [:S, L:]) = [:( Sigma S), ( Sigma L):] by Lm9;

      end;

      assume

       A3: for S be complete LATTICE holds the TopStruct of ( Sigma [:S, L:]) = [:( Sigma S), ( Sigma L):];

      let S be complete LATTICE;

       the TopStruct of ( Sigma [:S, L:]) = [:( Sigma S), ( Sigma L):] by A3;

      hence thesis by YELLOW_9: 51;

    end;

    theorem :: WAYBEL29:32

    

     Th32: for L be complete LATTICE holds (for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):]) iff for S be complete LATTICE holds ( Sigma [:S, L:]) = ( Omega [:( Sigma S), ( Sigma L):])

    proof

      let L be complete LATTICE;

      hereby

        assume

         A1: for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):];

        let S be complete LATTICE;

         the TopStruct of ( Sigma [:S, L:]) = [:( Sigma S), ( Sigma L):] by A1, Th31;

        then ( Omega ( Sigma [:S, L:])) = ( Omega [:( Sigma S), ( Sigma L):]) by WAYBEL25: 13;

        hence ( Sigma [:S, L:]) = ( Omega [:( Sigma S), ( Sigma L):]) by WAYBEL25: 15;

      end;

      assume

       A2: for S be complete LATTICE holds ( Sigma [:S, L:]) = ( Omega [:( Sigma S), ( Sigma L):]);

      let S be complete LATTICE;

      ( Sigma [:S, L:]) = ( Omega [:( Sigma S), ( Sigma L):]) by A2;

      then the TopStruct of ( Sigma [:S, L:]) = [:( Sigma S), ( Sigma L):] by WAYBEL25:def 2;

      hence thesis by YELLOW_9: 51;

    end;

    theorem :: WAYBEL29:33

    for L be complete LATTICE holds ( InclPoset ( sigma L)) is continuous iff for S be complete LATTICE holds ( Sigma [:S, L:]) = ( Omega [:( Sigma S), ( Sigma L):])

    proof

      let L be complete LATTICE;

      ( InclPoset ( sigma L)) is continuous iff for S be complete LATTICE holds ( sigma [:S, L:]) = the topology of [:( Sigma S), ( Sigma L):] by Th30;

      hence thesis by Th32;

    end;