lopclset.miz

    begin

    reserve T for non empty TopSpace,

X,Z for Subset of T;

    definition

      let T be non empty TopStruct;

      :: LOPCLSET:def1

      func OpenClosedSet (T) -> Subset-Family of T equals { x where x be Subset of T : x is open closed };

      coherence

      proof

        set A = { x where x be Subset of T : x is open closed };

        A c= ( bool the carrier of T)

        proof

          let y be object;

          assume y in A;

          then ex x be Subset of T st y = x & x is open & x is closed;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let T be non empty TopSpace;

      cluster ( OpenClosedSet T) -> non empty;

      coherence

      proof

        set A = { x where x be Subset of T : x is open closed };

        ( {} T) in A;

        hence thesis;

      end;

    end

    theorem :: LOPCLSET:1



     Th1: X in ( OpenClosedSet T) implies X is open

    proof

      assume X in ( OpenClosedSet T);

      then ex Z st Z = X & Z is open & Z is closed;

      hence thesis;

    end;

    theorem :: LOPCLSET:2



     Th2: X in ( OpenClosedSet T) implies X is closed

    proof

      assume X in ( OpenClosedSet T);

      then ex Z st Z = X & Z is open & Z is closed;

      hence thesis;

    end;

    theorem :: LOPCLSET:3



     Th3: X is open closed implies X in ( OpenClosedSet T);

    reserve x,y for Element of ( OpenClosedSet T);

    definition

      let T;

      let C,D be Element of ( OpenClosedSet T);

      :: original: \/

      redefine

      func C \/ D -> Element of ( OpenClosedSet T) ;

      coherence

      proof

        reconsider A = C, B = D as Subset of T;



         A1: A is open by Th1;



         A2: B is open by Th1;



         A3: A is closed by Th2;



         A4: B is closed by Th2;

        (A \/ B) is open by A1, A2;

        hence (C \/ D) is Element of ( OpenClosedSet T) by A3, A4, Th3;

      end;

      :: original: /\

      redefine

      func C /\ D -> Element of ( OpenClosedSet T) ;

      coherence

      proof

        reconsider A = C, B = D as Subset of T;



         A5: A is open by Th1;



         A6: B is open by Th1;



         A7: A is closed by Th2;



         A8: B is closed by Th2;

        (A /\ B) is open by A5, A6;

        hence (C /\ D) is Element of ( OpenClosedSet T) by A7, A8, Th3;

      end;

    end

    definition

      let T;

      deffunc U( Element of ( OpenClosedSet T), Element of ( OpenClosedSet T)) = ($1 \/ $2);

      :: LOPCLSET:def2

      func T_join T -> BinOp of ( OpenClosedSet T) means

      : Def2: for A,B be Element of ( OpenClosedSet T) holds (it . (A,B)) = (A \/ B);

      existence

      proof

        consider f be BinOp of ( OpenClosedSet T) such that

         A1: for x,y be Element of ( OpenClosedSet T) holds (f . (x,y)) = U(x,y) from BINOP_1:sch 4;

        take f;

        let x, y;

        thus thesis by A1;

      end;

      uniqueness

      proof

        thus for b1,b2 be BinOp of ( OpenClosedSet T) st (for A,B be Element of ( OpenClosedSet T) holds (b1 . (A,B)) = U(A,B)) & (for A,B be Element of ( OpenClosedSet T) holds (b2 . (A,B)) = U(A,B)) holds b1 = b2 from BINOP_2:sch 2;

      end;

      deffunc U( Element of ( OpenClosedSet T), Element of ( OpenClosedSet T)) = ($1 /\ $2);

      :: LOPCLSET:def3

      func T_meet T -> BinOp of ( OpenClosedSet T) means

      : Def3: for A,B be Element of ( OpenClosedSet T) holds (it . (A,B)) = (A /\ B);

      existence

      proof

        consider f be BinOp of ( OpenClosedSet T) such that

         A2: for x,y be Element of ( OpenClosedSet T) holds (f . (x,y)) = U(x,y) from BINOP_1:sch 4;

        take f;

        let x, y;

        thus thesis by A2;

      end;

      uniqueness

      proof

        thus for b1,b2 be BinOp of ( OpenClosedSet T) st (for A,B be Element of ( OpenClosedSet T) holds (b1 . (A,B)) = U(A,B)) & (for A,B be Element of ( OpenClosedSet T) holds (b2 . (A,B)) = U(A,B)) holds b1 = b2 from BINOP_2:sch 2;

      end;

    end

    theorem :: LOPCLSET:4

    for x,y be Element of LattStr (# ( OpenClosedSet T), ( T_join T), ( T_meet T) #), x9,y9 be Element of ( OpenClosedSet T) st x = x9 & y = y9 holds (x "\/" y) = (x9 \/ y9) by Def2;

    theorem :: LOPCLSET:5

    for x,y be Element of LattStr (# ( OpenClosedSet T), ( T_join T), ( T_meet T) #), x9,y9 be Element of ( OpenClosedSet T) st x = x9 & y = y9 holds (x "/\" y) = (x9 /\ y9) by Def3;

    theorem :: LOPCLSET:6

    ( {} T) is Element of ( OpenClosedSet T) by Th3;

    theorem :: LOPCLSET:7

    ( [#] T) is Element of ( OpenClosedSet T) by Th3;

    theorem :: LOPCLSET:8



     Th8: (x ` ) is Element of ( OpenClosedSet T)

    proof

      reconsider y = x as Subset of T;



       A1: y is open by Th1;

      y is closed by Th2;

      then

       A2: (x ` ) is open;

      (x ` ) is closed by A1;

      hence thesis by A2, Th3;

    end;

    theorem :: LOPCLSET:9



     Th9: LattStr (# ( OpenClosedSet T), ( T_join T), ( T_meet T) #) is Lattice

    proof

      set L = LattStr (# ( OpenClosedSet T), ( T_join T), ( T_meet T) #);



       A1: for p,q be Element of L holds (p "\/" q) = (q "\/" p)

      proof

        let p,q be Element of L;

        consider p9,q9 be Element of ( OpenClosedSet T) such that

         A2: p = p9 and

         A3: q = q9;



        thus (p "\/" q) = (q9 \/ p9) by A2, A3, Def2

        .= (q "\/" p) by A2, A3, Def2;

      end;



       A4: for p,q,r be Element of L holds (p "\/" (q "\/" r)) = ((p "\/" q) "\/" r)

      proof

        let p,q,r be Element of L;

        consider p9,q9,r9,k9,l9 be Element of ( OpenClosedSet T) such that

         A5: p = p9 and

         A6: q = q9 and

         A7: r = r9 and

         A8: (q "\/" r) = k9 and

         A9: (p "\/" q) = l9;



        thus (p "\/" (q "\/" r)) = (p9 \/ k9) by A5, A8, Def2

        .= (p9 \/ (q9 \/ r9)) by A6, A7, A8, Def2

        .= ((p9 \/ q9) \/ r9) by XBOOLE_1: 4

        .= (l9 \/ r9) by A5, A6, A9, Def2

        .= ((p "\/" q) "\/" r) by A7, A9, Def2;

      end;



       A10: for p,q be Element of L holds ((p "/\" q) "\/" q) = q

      proof

        let p,q be Element of L;

        consider p9,q9,k9 be Element of ( OpenClosedSet T) such that

         A11: p = p9 and

         A12: q = q9 and

         A13: (p "/\" q) = k9;



        thus ((p "/\" q) "\/" q) = (k9 \/ q9) by A12, A13, Def2

        .= ((p9 /\ q9) \/ q9) by A11, A12, A13, Def3

        .= q by A12, XBOOLE_1: 22;

      end;



       A14: for p,q be Element of L holds (p "/\" q) = (q "/\" p)

      proof

        let p,q be Element of L;

        consider p9,q9 be Element of ( OpenClosedSet T) such that

         A15: p = p9 and

         A16: q = q9;



        thus (p "/\" q) = (q9 /\ p9) by A15, A16, Def3

        .= (q "/\" p) by A15, A16, Def3;

      end;



       A17: for p,q,r be Element of L holds (p "/\" (q "/\" r)) = ((p "/\" q) "/\" r)

      proof

        let p,q,r be Element of L;

        consider p9,q9,r9,k9,l9 be Element of ( OpenClosedSet T) such that

         A18: p = p9 and

         A19: q = q9 and

         A20: r = r9 and

         A21: (q "/\" r) = k9 and

         A22: (p "/\" q) = l9;



        thus (p "/\" (q "/\" r)) = (p9 /\ k9) by A18, A21, Def3

        .= (p9 /\ (q9 /\ r9)) by A19, A20, A21, Def3

        .= ((p9 /\ q9) /\ r9) by XBOOLE_1: 16

        .= (l9 /\ r9) by A18, A19, A22, Def3

        .= ((p "/\" q) "/\" r) by A20, A22, Def3;

      end;

      for p,q be Element of L holds (p "/\" (p "\/" q)) = p

      proof

        let p,q be Element of L;

        consider p9,q9,k9 be Element of ( OpenClosedSet T) such that

         A23: p = p9 and

         A24: q = q9 and

         A25: (p "\/" q) = k9;



        thus (p "/\" (p "\/" q)) = (p9 /\ k9) by A23, A25, Def3

        .= (p9 /\ (p9 \/ q9)) by A23, A24, A25, Def2

        .= p by A23, XBOOLE_1: 21;

      end;

      then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A4, A10, A14, A17;

      hence thesis;

    end;

    definition

      let T be non empty TopSpace;

      :: LOPCLSET:def4

      func OpenClosedSetLatt (T) -> Lattice equals LattStr (# ( OpenClosedSet T), ( T_join T), ( T_meet T) #);

      coherence by Th9;

    end

    theorem :: LOPCLSET:10

    for T be non empty TopSpace, x,y be Element of ( OpenClosedSetLatt T) holds (x "\/" y) = (x \/ y) by Def2;

    theorem :: LOPCLSET:11

    for T be non empty TopSpace, x,y be Element of ( OpenClosedSetLatt T) holds (x "/\" y) = (x /\ y) by Def3;

    theorem :: LOPCLSET:12

    the carrier of ( OpenClosedSetLatt T) = ( OpenClosedSet T);

    registration

      let T;

      cluster ( OpenClosedSetLatt T) -> Boolean;

      coherence

      proof

        set OCL = ( OpenClosedSetLatt T);



         A1: for a,b,c be Element of OCL holds (a "/\" (b "\/" c)) = ((a "/\" b) "\/" (a "/\" c))

        proof

          let a,b,c be Element of OCL;

          set m = (a "/\" c);

          consider a9,b9,c9,k9,l9,m9 be Element of ( OpenClosedSet T) such that

           A2: a = a9 and

           A3: b = b9 and

           A4: c = c9 and

           A5: (b "\/" c) = k9 and

           A6: (a "/\" b) = l9 and

           A7: m = m9;



           A8: (a9 /\ c9) = m by A2, A4, Def3;



          thus (a "/\" (b "\/" c)) = (a9 /\ k9) by A2, A5, Def3

          .= (a9 /\ (b9 \/ c9)) by A3, A4, A5, Def2

          .= ((a9 /\ b9) \/ (a9 /\ c9)) by XBOOLE_1: 23

          .= (l9 \/ m9) by A2, A3, A6, A7, A8, Def3

          .= ((a "/\" b) "\/" (a "/\" c)) by A6, A7, Def2;

        end;

        reconsider bot = ( {} T) as Element of OCL by Th3;

        reconsider top = ( [#] T) as Element of OCL by Th3;



         A9: for a be Element of OCL holds (top "\/" a) = top & (a "\/" top) = top

        proof

          let a be Element of OCL;

          reconsider a9 = a as Element of ( OpenClosedSet T);



          thus (top "\/" a) = (( [#] T) \/ a9) by Def2

          .= top by XBOOLE_1: 12;

          hence thesis;

        end;



         A10: for a be Element of OCL holds (bot "/\" a) = bot & (a "/\" bot) = bot

        proof

          let a be Element of OCL;

          reconsider a9 = a as Element of ( OpenClosedSet T);



          thus (bot "/\" a) = ( {} /\ a9) by Def3

          .= bot;

          hence thesis;

        end;

        then

         A11: OCL is lower-bounded;



         A12: OCL is upper-bounded by A9;



         A13: ( {} T) = ( Bottom OCL) by A10, A11, LATTICES:def 16;



         A14: ( [#] T) = ( Top OCL) by A9, A12, LATTICES:def 17;

        thus OCL is bounded by A11, A12;

        reconsider OCL as 01_Lattice by A11, A12;

        for b be Element of OCL holds ex a be Element of OCL st a is_a_complement_of b

        proof

          let b be Element of OCL;

          reconsider c = b as Element of ( OpenClosedSet T);

          reconsider a = (c ` ) as Element of OCL by Th8;



           A15: (a "\/" b) = (c \/ (c ` )) by Def2

          .= ( Top OCL) by A14, PRE_TOPC: 2;



           A16: c misses (c ` ) by XBOOLE_1: 79;



           A17: (a "/\" b) = (c /\ (c ` )) by Def3

          .= ( Bottom OCL) by A13, A16;

          take a;

          (a "\/" b) = (b "\/" a) & (a "/\" b) = (b "/\" a);

          hence thesis by A15, A17;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: LOPCLSET:13

    ( [#] T) is Element of ( OpenClosedSetLatt T) by Th3;

    theorem :: LOPCLSET:14

    ( {} T) is Element of ( OpenClosedSetLatt T) by Th3;

    reserve x,y,X for set;

    registration

      cluster non trivial for B_Lattice;

      existence

      proof

        set T = the non empty TopSpace;

        reconsider E = ( OpenClosedSetLatt T) as B_Lattice;

        reconsider a = ( [#] T), b = ( {} T) as Element of E by Th3;

        take E, a, b;

        thus thesis;

      end;

    end

    reserve BL for non trivial B_Lattice,

a,b,c,p,q for Element of BL,

UF,F,F0,F1,F2 for Filter of BL;

    definition

      let BL;

      :: LOPCLSET:def5

      func ultraset BL -> Subset-Family of BL equals { F : F is being_ultrafilter };

      coherence

      proof

        set US = { F : F is being_ultrafilter };

        US c= ( bool the carrier of BL)

        proof

          let x be object;

          assume x in US;

          then ex UF st (UF = x) & (UF is being_ultrafilter);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let BL;

      cluster ( ultraset BL) -> non empty;

      coherence

      proof

        set US = { F : F is being_ultrafilter };

        consider p1,p2 be Element of BL such that

         A1: p1 <> p2 by STRUCT_0:def 10;

        p1 <> ( Bottom BL) or p2 <> ( Bottom BL) by A1;

        then

        consider p be Element of BL such that

         A2: p <> ( Bottom BL);

        consider H be Filter of BL such that p in H and

         A3: H is being_ultrafilter by A2, FILTER_0: 20;

        H in US by A3;

        hence thesis;

      end;

    end

    theorem :: LOPCLSET:15

    x in ( ultraset BL) iff ex UF st UF = x & UF is being_ultrafilter;

    theorem :: LOPCLSET:16



     Th16: for a holds { F : F is being_ultrafilter & a in F } c= ( ultraset BL)

    proof

      let a;

      let x be object;

      assume x in { F : F is being_ultrafilter & a in F };

      then ex UF st (UF = x) & (UF is being_ultrafilter) & (a in UF);

      hence thesis;

    end;

    definition

      let BL;

      :: LOPCLSET:def6

      func UFilter BL -> Function means

      : Def6: ( dom it ) = the carrier of BL & for a be Element of BL holds (it . a) = { UF : UF is being_ultrafilter & a in UF };

      existence

      proof

        deffunc U( object) = { F : F is being_ultrafilter & $1 in F };

        consider f be Function such that

         A1: ( dom f) = the carrier of BL and

         A2: for x be object st x in the carrier of BL holds (f . x) = U(x) from FUNCT_1:sch 3;

        take f;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let f1,f2 be Function;

        assume that

         A3: ( dom f1) = the carrier of BL & for a holds (f1 . a) = { F : F is being_ultrafilter & a in F } and

         A4: ( dom f2) = the carrier of BL & for a holds (f2 . a) = { F : F is being_ultrafilter & a in F };

        now

          let x be object;

          assume x in the carrier of BL;

          then

          reconsider a = x as Element of BL;



          thus (f1 . x) = { F : F is being_ultrafilter & a in F } by A3

          .= (f2 . x) by A4;

        end;

        hence thesis by A3, A4, FUNCT_1: 2;

      end;

    end

    theorem :: LOPCLSET:17



     Th17: x in (( UFilter BL) . a) iff ex F st F = x & F is being_ultrafilter & a in F

    proof



       A1: x in (( UFilter BL) . a) implies ex F st F = x & F is being_ultrafilter & a in F

      proof

        assume x in (( UFilter BL) . a);

        then x in { UF : UF is being_ultrafilter & a in UF } by Def6;

        then

        consider F such that

         A2: F = x and

         A3: F is being_ultrafilter and

         A4: a in F;

        take F;

        thus thesis by A2, A3, A4;

      end;

      (ex F st F = x & F is being_ultrafilter & a in F) implies x in (( UFilter BL) . a)

      proof

        assume ex F st F = x & F is being_ultrafilter & a in F;

        then x in { UF : UF is being_ultrafilter & a in UF };

        hence thesis by Def6;

      end;

      hence thesis by A1;

    end;

    theorem :: LOPCLSET:18



     Th18: F in (( UFilter BL) . a) iff F is being_ultrafilter & a in F

    proof

      hereby

        assume F in (( UFilter BL) . a);

        then ex F0 st (F0 = F) & (F0 is being_ultrafilter) & (a in F0) by Th17;

        hence F is being_ultrafilter & a in F;

      end;

      thus thesis by Th17;

    end;

    theorem :: LOPCLSET:19



     Th19: for F st F is being_ultrafilter holds (a "\/" b) in F iff a in F or b in F

    proof

      let F;

      assume F is being_ultrafilter;

      then F is prime by FILTER_0: 45;

      hence thesis by FILTER_0:def 5;

    end;

    theorem :: LOPCLSET:20



     Th20: (( UFilter BL) . (a "/\" b)) = ((( UFilter BL) . a) /\ (( UFilter BL) . b))

    proof



       A1: (( UFilter BL) . (a "/\" b)) c= ((( UFilter BL) . a) /\ (( UFilter BL) . b))

      proof

        let x be object;

        set c = (a "/\" b);

        assume x in (( UFilter BL) . c);

        then

        consider F0 such that

         A2: x = F0 and

         A3: F0 is being_ultrafilter and

         A4: c in F0 by Th17;



         A5: a in F0 by A4, FILTER_0: 8;



         A6: b in F0 by A4, FILTER_0: 8;



         A7: F0 in (( UFilter BL) . a) by A3, A5, Th17;

        F0 in (( UFilter BL) . b) by A3, A6, Th17;

        hence thesis by A2, A7, XBOOLE_0:def 4;

      end;

      ((( UFilter BL) . a) /\ (( UFilter BL) . b)) c= (( UFilter BL) . (a "/\" b))

      proof

        let x be object;

        assume

         A8: x in ((( UFilter BL) . a) /\ (( UFilter BL) . b));

        then

         A9: x in (( UFilter BL) . a) by XBOOLE_0:def 4;



         A10: x in (( UFilter BL) . b) by A8, XBOOLE_0:def 4;



         A11: ex F0 st x = F0 & F0 is being_ultrafilter & a in F0 by A9, Th17;

        ex F0 st x = F0 & F0 is being_ultrafilter & b in F0 by A10, Th17;

        then

        consider F0 such that

         A12: x = F0 and

         A13: F0 is being_ultrafilter and

         A14: a in F0 and

         A15: b in F0 by A11;

        (a "/\" b) in F0 by A14, A15, FILTER_0: 8;

        hence thesis by A12, A13, Th17;

      end;

      hence thesis by A1;

    end;

    theorem :: LOPCLSET:21



     Th21: (( UFilter BL) . (a "\/" b)) = ((( UFilter BL) . a) \/ (( UFilter BL) . b))

    proof



       A1: (( UFilter BL) . (a "\/" b)) c= ((( UFilter BL) . a) \/ (( UFilter BL) . b))

      proof

        let x be object;

        set c = (a "\/" b);

        assume x in (( UFilter BL) . c);

        then

        consider F0 such that

         A2: x = F0 and

         A3: F0 is being_ultrafilter and

         A4: c in F0 by Th17;

        a in F0 or b in F0 by A3, A4, Th19;

        then F0 in (( UFilter BL) . a) or F0 in (( UFilter BL) . b) by A3, Th17;

        hence thesis by A2, XBOOLE_0:def 3;

      end;

      ((( UFilter BL) . a) \/ (( UFilter BL) . b)) c= (( UFilter BL) . (a "\/" b))

      proof

        let x be object;

        assume x in ((( UFilter BL) . a) \/ (( UFilter BL) . b));

        then x in (( UFilter BL) . a) or x in (( UFilter BL) . b) by XBOOLE_0:def 3;

        then (ex F0 st x = F0 & F0 is being_ultrafilter & a in F0) or ex F0 st x = F0 & F0 is being_ultrafilter & b in F0 by Th17;

        then

        consider F0 such that

         A5: x = F0 and

         A6: F0 is being_ultrafilter and

         A7: a in F0 or b in F0;

        (a "\/" b) in F0 by A6, A7, Th19;

        hence thesis by A5, A6, Th17;

      end;

      hence thesis by A1;

    end;

    definition

      let BL;

      :: original: UFilter

      redefine

      func UFilter BL -> Function of the carrier of BL, ( bool ( ultraset BL)) ;

      coherence

      proof

        reconsider f = ( UFilter BL) as Function;



         A1: ( dom f) = the carrier of BL by Def6;

        ( rng f) c= ( bool ( ultraset BL))

        proof

          let y be object;

          reconsider yy = y as set by TARSKI: 1;

          assume y in ( rng f);

          then

          consider x be object such that

           A2: x in ( dom f) and

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

          y = { F : F is being_ultrafilter & x in F } by A1, A2, A3, Def6;

          then yy c= ( ultraset BL) by A1, A2, Th16;

          hence thesis;

        end;

        then

        reconsider f as Function of the carrier of BL, ( bool ( ultraset BL)) by A1, FUNCT_2:def 1, RELSET_1: 4;

        for a holds (f . a) = { F : F is being_ultrafilter & a in F } by Def6;

        hence thesis;

      end;

    end

    definition

      let BL;

      :: LOPCLSET:def7

      func StoneR BL -> set equals ( rng ( UFilter BL));

      coherence ;

    end

    registration

      let BL;

      cluster ( StoneR BL) -> non empty;

      coherence ;

    end

    theorem :: LOPCLSET:22

    ( StoneR BL) c= ( bool ( ultraset BL));

    theorem :: LOPCLSET:23



     Th23: x in ( StoneR BL) iff ex a st (( UFilter BL) . a) = x

    proof



       A1: x in ( StoneR BL) implies ex a st (( UFilter BL) . a) = x

      proof

        assume x in ( StoneR BL);

        then

        consider y be object such that

         A2: y in ( dom ( UFilter BL)) and

         A3: x = (( UFilter BL) . y) by FUNCT_1:def 3;

        reconsider a = y as Element of BL by A2;

        take a;

        thus thesis by A3;

      end;

      (ex a st (( UFilter BL) . a) = x) implies x in ( StoneR BL)

      proof

        given a such that

         A4: x = (( UFilter BL) . a);

        a in the carrier of BL;

        then a in ( dom ( UFilter BL)) by Def6;

        hence thesis by A4, FUNCT_1:def 3;

      end;

      hence thesis by A1;

    end;

    definition

      let BL;

      :: LOPCLSET:def8

      func StoneSpace BL -> strict TopSpace means

      : Def8: the carrier of it = ( ultraset BL) & the topology of it = { ( union A) where A be Subset-Family of ( ultraset BL) : A c= ( StoneR BL) };

      existence

      proof

        set US = ( ultraset BL);

        set STP = { ( union A) where A be Subset-Family of ( ultraset BL) : A c= ( StoneR BL) };

        STP c= ( bool US)

        proof

          let x be object;

          assume x in STP;

          then ex B be Subset-Family of ( ultraset BL) st (x = ( union B)) & (B c= ( StoneR BL));

          hence thesis;

        end;

        then

        reconsider STP = { ( union A) where A be Subset-Family of ( ultraset BL) : A c= ( StoneR BL) } as Subset-Family of US;

         TopStruct (# US, STP #) is strict TopSpace

        proof

          set TS = TopStruct (# US, STP #);



           A1: the carrier of TS in the topology of TS

          proof

            set B = { F : F is being_ultrafilter & ( Top BL) in F };

            B c= ( ultraset BL)

            proof

              let x be object;

              assume x in B;

              then ex F st F = x & F is being_ultrafilter & ( Top BL) in F;

              hence thesis;

            end;

            then

             A2: ( bool B) c= ( bool ( ultraset BL)) by ZFMISC_1: 67;

             {B} c= ( bool B) by ZFMISC_1: 68;

            then

            reconsider SB = {B} as Subset-Family of ( ultraset BL) by A2, XBOOLE_1: 1;

            reconsider SB as Subset-Family of ( ultraset BL);



             A3: ( union SB) = B by ZFMISC_1: 25;

            ( ultraset BL) c= B

            proof

              let x be object;

              assume x in ( ultraset BL);

              then

              consider F such that

               A4: F = x and

               A5: F is being_ultrafilter;

              ( Top BL) in F by FILTER_0: 11;

              hence thesis by A4, A5;

            end;

            then

             A6: ( ultraset BL) = ( union SB) by A3;

            (( UFilter BL) . ( Top BL)) = { F : F is being_ultrafilter & ( Top BL) in F } by Def6;

            then B in ( StoneR BL) by Th23;

            then SB c= ( StoneR BL) by ZFMISC_1: 31;

            hence thesis by A6;

          end;



           A7: for a be Subset-Family of TS st a c= the topology of TS holds ( union a) in the topology of TS

          proof

            let a be Subset-Family of TS;

            assume

             A8: a c= the topology of TS;

            set B = { A where A be Subset of ( StoneR BL) : ( union A) in a };

            B c= ( bool ( StoneR BL))

            proof

              let x be object;

              assume x in B;

              then ex C be Subset of ( StoneR BL) st C = x & ( union C) in a;

              then

              reconsider C = x as Subset of ( StoneR BL);

              C c= ( StoneR BL);

              hence thesis;

            end;

            then

            reconsider BS = B as Subset-Family of ( StoneR BL);



             A9: ( union ( union BS)) = ( union { ( union A) where A be Subset of ( StoneR BL) : A in BS }) by EQREL_1: 54;



             A10: a c= { ( union A) where A be Subset of ( StoneR BL) : A in BS }

            proof

              let x be object;

              assume

               A11: x in a;

              then x in STP by A8;

              then

              consider C be Subset-Family of ( ultraset BL) such that

               A12: x = ( union C) and

               A13: C c= ( StoneR BL);

              C in BS by A11, A12, A13;

              hence thesis by A12;

            end;

            { ( union A) where A be Subset of ( StoneR BL) : A in BS } c= a

            proof

              let x be object;

              assume x in { ( union A) where A be Subset of ( StoneR BL) : A in BS };

              then

              consider C be Subset of ( StoneR BL) such that

               A14: ( union C) = x and

               A15: C in BS;

              ex D be Subset of ( StoneR BL) st (D = C) & (( union D) in a) by A15;

              hence thesis by A14;

            end;

            then

             A16: a = { ( union A) where A be Subset of ( StoneR BL) : A in BS } by A10;

            ( union BS) is Subset-Family of ( ultraset BL) by XBOOLE_1: 1;

            hence thesis by A9, A16;

          end;

          for p,q be Subset of TS st p in the topology of TS & q in the topology of TS holds (p /\ q) in the topology of TS

          proof

            let p,q be Subset of TS;

            assume that

             A17: p in the topology of TS and

             A18: q in the topology of TS;

            consider P be Subset-Family of ( ultraset BL) such that

             A19: ( union P) = p and

             A20: P c= ( StoneR BL) by A17;

            consider Q be Subset-Family of ( ultraset BL) such that

             A21: ( union Q) = q and

             A22: Q c= ( StoneR BL) by A18;



             A23: (( union P) /\ ( union Q)) = ( union ( INTERSECTION (P,Q))) by SETFAM_1: 28;

            ( INTERSECTION (P,Q)) c= ( bool ( ultraset BL))

            proof

              let x be object;

              assume x in ( INTERSECTION (P,Q));

              then

              consider X,Y be set such that

               A24: X in P and

               A25: Y in Q and

               A26: x = (X /\ Y) by SETFAM_1:def 5;



               A27: (X /\ Y) c= (X \/ Y) by XBOOLE_1: 29;

              (X \/ Y) c= ( ultraset BL) by A24, A25, XBOOLE_1: 8;

              then (X /\ Y) c= ( ultraset BL) by A27;

              hence thesis by A26;

            end;

            then

            reconsider C = ( INTERSECTION (P,Q)) as Subset-Family of ( ultraset BL);

            reconsider C as Subset-Family of ( ultraset BL);

            C c= ( StoneR BL)

            proof

              let x be object;

              assume x in C;

              then

              consider X,Y be set such that

               A28: X in P and

               A29: Y in Q and

               A30: x = (X /\ Y) by SETFAM_1:def 5;

              consider a such that

               A31: X = (( UFilter BL) . a) by A20, A28, Th23;

              consider b such that

               A32: Y = (( UFilter BL) . b) by A22, A29, Th23;



               A33: X = { F : F is being_ultrafilter & a in F } by A31, Def6;



               A34: Y = { F : F is being_ultrafilter & b in F } by A32, Def6;



               A35: (X /\ Y) = { F : F is being_ultrafilter & (a "/\" b) in F }

              proof



                 A36: (X /\ Y) c= { F : F is being_ultrafilter & (a "/\" b) in F }

                proof

                  let x be object;

                  assume

                   A37: x in (X /\ Y);

                  then

                   A38: x in X by XBOOLE_0:def 4;



                   A39: x in Y by A37, XBOOLE_0:def 4;

                  consider F1 such that

                   A40: x = F1 and

                   A41: F1 is being_ultrafilter and

                   A42: a in F1 by A33, A38;

                  ex F2 st (x = F2) & (F2 is being_ultrafilter) & (b in F2) by A34, A39;

                  then (a "/\" b) in F1 by A40, A42, FILTER_0: 8;

                  hence thesis by A40, A41;

                end;

                { F : F is being_ultrafilter & (a "/\" b) in F } c= (X /\ Y)

                proof

                  let x be object;

                  assume x in { F : F is being_ultrafilter & (a "/\" b) in F };

                  then

                  consider F0 such that

                   A43: x = F0 and

                   A44: F0 is being_ultrafilter and

                   A45: (a "/\" b) in F0;

                  a in F0 by A45, FILTER_0: 8;

                  then

                  consider F such that

                   A46: F = F0 and

                   A47: F is being_ultrafilter and

                   A48: a in F by A44;



                   A49: F in X by A33, A47, A48;

                  b in F0 by A45, FILTER_0: 8;

                  then

                  consider F1 such that

                   A50: F1 = F0 and

                   A51: F1 is being_ultrafilter and

                   A52: b in F1 by A44;

                  F1 in Y by A34, A51, A52;

                  hence thesis by A43, A46, A49, A50, XBOOLE_0:def 4;

                end;

                hence thesis by A36;

              end;

              (( UFilter BL) . (a "/\" b)) = { F : F is being_ultrafilter & (a "/\" b) in F } by Def6;

              hence thesis by A30, A35, Th23;

            end;

            hence thesis by A19, A21, A23;

          end;

          hence thesis by A1, A7, PRE_TOPC:def 1;

        end;

        then

        reconsider TS = TopStruct (# US, STP #) as strict TopSpace;

        take TS;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let BL;

      cluster ( StoneSpace BL) -> non empty;

      coherence

      proof

        the carrier of ( StoneSpace BL) = ( ultraset BL) by Def8;

        hence the carrier of ( StoneSpace BL) is non empty;

      end;

    end

    theorem :: LOPCLSET:24

    F is being_ultrafilter & not F in (( UFilter BL) . a) implies not a in F by Th18;

    theorem :: LOPCLSET:25



     Th25: (( ultraset BL) \ (( UFilter BL) . a)) = (( UFilter BL) . (a ` ))

    proof

      hereby

        let x be object;

        assume

         A1: x in (( ultraset BL) \ (( UFilter BL) . a));

        then

         A2: x in ( ultraset BL) by XBOOLE_0:def 5;



         A3: not x in (( UFilter BL) . a) by A1, XBOOLE_0:def 5;

        consider F such that

         A4: F = x and

         A5: F is being_ultrafilter by A2;

         not a in F by A3, A4, A5, Th18;

        then (a ` ) in F by A5, FILTER_0: 46;

        hence x in (( UFilter BL) . (a ` )) by A4, A5, Th18;

      end;

      let x be object;

      assume x in (( UFilter BL) . (a ` ));

      then

      consider F such that

       A6: F = x and

       A7: F is being_ultrafilter and

       A8: (a ` ) in F by Th17;



       A9: not a in F by A7, A8, FILTER_0: 46;



       A10: F in ( ultraset BL) by A7;

       not F in (( UFilter BL) . a) by A9, Th18;

      hence x in (( ultraset BL) \ (( UFilter BL) . a)) by A6, A10, XBOOLE_0:def 5;

    end;

    definition

      let BL;

      :: LOPCLSET:def9

      func StoneBLattice BL -> Lattice equals ( OpenClosedSetLatt ( StoneSpace BL));

      coherence ;

    end



     Lm1: for p be Subset of ( StoneSpace BL) holds p in ( StoneR BL) implies p is open

    proof

      let p be Subset of ( StoneSpace BL);

      assume

       A1: p in ( StoneR BL);

      then

       A2: {p} is Subset-Family of ( ultraset BL) by SUBSET_1: 41;



       A3: {p} c= ( StoneR BL) by A1, ZFMISC_1: 31;

      ( union {p}) = p by ZFMISC_1: 25;

      then p in { ( union A) where A be Subset-Family of ( ultraset BL) : A c= ( StoneR BL) } by A2, A3;

      then p in the topology of ( StoneSpace BL) by Def8;

      hence thesis by PRE_TOPC:def 2;

    end;

    registration

      let BL;

      cluster ( UFilter BL) -> one-to-one;

      coherence

      proof

        now

          let a, b;

          assume that

           A1: (( UFilter BL) . a) = (( UFilter BL) . b);

          assume not a = b;

          then

          consider UF such that

           A2: UF is being_ultrafilter and

           A3: a in UF & not b in UF or not a in UF & b in UF by FILTER_0: 47;

          now

            per cases by A3;

              case

               A4: a in UF & not b in UF;

              then UF in (( UFilter BL) . a) by A2, Th18;

              hence (( UFilter BL) . a) <> (( UFilter BL) . b) by A4, Th18;

            end;

              case not a in UF & b in UF;

              then not UF in (( UFilter BL) . a) by Th18;

              hence (( UFilter BL) . a) <> (( UFilter BL) . b) by A2, A3, Th18;

            end;

          end;

          hence contradiction by A1;

        end;

        hence thesis by GROUP_6: 1;

      end;

    end

    theorem :: LOPCLSET:26

    ( union ( StoneR BL)) = ( ultraset BL)

    proof

      set x = the Element of ( OpenClosedSet ( StoneSpace BL));

      reconsider X = x as Subset of ( StoneSpace BL);



       A1: X is open by Th1;



       A2: X is closed by Th2;

      X in the topology of ( StoneSpace BL) by A1, PRE_TOPC:def 2;

      then X in { ( union A) where A be Subset-Family of ( ultraset BL) : A c= ( StoneR BL) } by Def8;

      then

      consider B be Subset-Family of ( ultraset BL) such that

       A3: ( union B) = X and

       A4: B c= ( StoneR BL);

      (X ` ) is open by A2;

      then (X ` ) in the topology of ( StoneSpace BL) by PRE_TOPC:def 2;

      then (X ` ) in { ( union A) where A be Subset-Family of ( ultraset BL) : A c= ( StoneR BL) } by Def8;

      then

      consider C be Subset-Family of ( ultraset BL) such that

       A5: ( union C) = (X ` ) and

       A6: C c= ( StoneR BL);

      (B \/ C) c= ( StoneR BL) by A4, A6, XBOOLE_1: 8;

      then ( union (B \/ C)) c= ( union ( StoneR BL)) by ZFMISC_1: 77;

      then (X \/ (X ` )) c= ( union ( StoneR BL)) by A3, A5, ZFMISC_1: 78;

      then ( [#] ( StoneSpace BL)) c= ( union ( StoneR BL)) by PRE_TOPC: 2;

      then

       A7: ( ultraset BL) c= ( union ( StoneR BL)) by Def8;

      ( union ( StoneR BL)) c= ( union ( bool ( ultraset BL))) by ZFMISC_1: 77;

      then ( union ( StoneR BL)) c= ( ultraset BL) by ZFMISC_1: 81;

      hence thesis by A7;

    end;

    theorem :: LOPCLSET:27



     Th27: for X be non empty set holds ex Y be Element of ( Fin X) st Y is non empty

    proof

      let X be non empty set;

      set a = the Element of X;

       {.a.} is Element of ( Fin X);

      hence thesis;

    end;

    registration

      let D be non empty set;

      cluster non empty for Element of ( Fin D);

      existence by Th27;

    end

    theorem :: LOPCLSET:28



     Th28: for L be non trivial B_Lattice, D be non empty Subset of L st ( Bottom L) in <.D.) holds ex B be non empty Element of ( Fin the carrier of L) st B c= D & ( FinMeet B) = ( Bottom L)

    proof

      let L be non trivial B_Lattice, D be non empty Subset of L such that

       A1: ( Bottom L) in <.D.);

      set A = { ( FinMeet C) where C be Element of ( Fin the carrier of L) : C c= D & C <> {} };

      set AA = { a where a be Element of L : ex c be Element of L st c in A & c [= a };



       A2: AA c= the carrier of L

      proof

        let x be object;

        assume x in AA;

        then ex a be Element of L st (a = x) & (ex c be Element of L st c in A & c [= a);

        hence thesis;

      end;

      AA is non empty

      proof

        consider C be Element of ( Fin D) such that

         A3: C is non empty by Th27;



         A4: C is Subset of D by FINSUB_1: 16;

        then C c= the carrier of L by XBOOLE_1: 1;

        then C is Element of ( Fin the carrier of L) by FINSUB_1:def 5;

        then

        consider C be Element of ( Fin the carrier of L) such that

         A5: C <> {} and

         A6: C c= D by A3, A4;

        reconsider a = ( FinMeet C) as Element of L;

        a in A by A5, A6;

        then a in AA;

        hence thesis;

      end;

      then

      reconsider AA as non empty Subset of L by A2;



       A7: for p,q be Element of L st p in AA & q in AA holds (p "/\" q) in AA

      proof

        let p,q be Element of L;

        assume that

         A8: p in AA and

         A9: q in AA;

        consider a be Element of L such that

         A10: a = p and

         A11: ex c be Element of L st c in A & c [= a by A8;

        consider c be Element of L such that

         A12: c in A and

         A13: c [= a by A11;

        consider b be Element of L such that

         A14: b = q and

         A15: ex d be Element of L st d in A & d [= b by A9;

        consider d be Element of L such that

         A16: d in A and

         A17: d [= b by A15;



         A18: (c "/\" d) [= (a "/\" b) by A13, A17, FILTER_0: 5;

        consider C be Element of ( Fin the carrier of L) such that

         A19: c = ( FinMeet C) and

         A20: C c= D and

         A21: C <> {} by A12;

        consider E be Element of ( Fin the carrier of L) such that

         A22: d = ( FinMeet E) and

         A23: E c= D and E <> {} by A16;



         A24: (c "/\" d) = ( FinMeet (C \/ E)) by A19, A22, LATTICE4: 23;

        (C \/ E) c= D by A20, A23, XBOOLE_1: 8;

        then (c "/\" d) in A by A21, A24;

        hence thesis by A10, A14, A18;

      end;

      for p,q be Element of L st p in AA & p [= q holds q in AA

      proof

        let p,q be Element of L;

        assume that

         A25: p in AA and

         A26: p [= q;



         A27: ex a be Element of L st (a = p) & (ex c be Element of L st c in A & c [= a) by A25;

        ex b be Element of L st (b = q) & (ex c be Element of L st c in A & c [= b) by A26, A27, LATTICES: 7;

        hence thesis;

      end;

      then

       A28: AA is Filter of L by A7, FILTER_0: 9;

      D c= AA

      proof

        let x be object;

        assume

         A29: x in D;

        then

         A30: {x} c= D by ZFMISC_1: 31;

         {x} c= the carrier of L by A29, ZFMISC_1: 31;

        then

        reconsider C = {x} as Element of ( Fin the carrier of L) by FINSUB_1:def 5;



         A31: x = (( id the carrier of L) . x) by A29, FUNCT_1: 18

        .= (the L_meet of L $$ (C,( id the carrier of L))) by A29, SETWISEO: 17

        .= ( FinMeet (C,( id L))) by LATTICE2:def 4

        .= ( FinMeet C) by LATTICE4:def 9;

        reconsider a = ( FinMeet C) as Element of L;

        a in A by A30;

        hence thesis by A31;

      end;

      then <.D.) c= AA by A28, FILTER_0:def 4;

      then ( Bottom L) in AA by A1;

      then ex d be Element of L st d = ( Bottom L) & ex c be Element of L st c in A & c [= d;

      then

      consider c be Element of L such that

       A32: c in A and

       A33: c [= ( Bottom L);

      ( Bottom L) [= c;

      then ( Bottom L) in A by A32, A33, LATTICES: 8;

      then ex C be Element of ( Fin the carrier of L) st ( Bottom L) = ( FinMeet C) & C c= D & C <> {} ;

      hence thesis;

    end;

    theorem :: LOPCLSET:29



     Th29: for L be 0_Lattice holds not ex F be Filter of L st F is being_ultrafilter & ( Bottom L) in F

    proof

      let L be 0_Lattice;

      given F be Filter of L such that

       A1: F is being_ultrafilter and

       A2: ( Bottom L) in F;

      F = the carrier of L by A2, FILTER_0: 26;

      hence contradiction by A1, FILTER_0:def 3;

    end;

    theorem :: LOPCLSET:30



     Th30: (( UFilter BL) . ( Bottom BL)) = {}

    proof

      assume

       A1: (( UFilter BL) . ( Bottom BL)) <> {} ;

      set x = the Element of (( UFilter BL) . ( Bottom BL));

      ex F st F = x & F is being_ultrafilter & ( Bottom BL) in F by A1, Th17;

      hence contradiction by Th29;

    end;

    theorem :: LOPCLSET:31

    (( UFilter BL) . ( Top BL)) = ( ultraset BL)

    proof



      thus (( UFilter BL) . ( Top BL)) = (( UFilter BL) . (( Bottom BL) ` )) by LATTICE4: 30

      .= (( ultraset BL) \ (( UFilter BL) . ( Bottom BL))) by Th25

      .= (( ultraset BL) \ {} ) by Th30

      .= ( ultraset BL);

    end;

    theorem :: LOPCLSET:32



     Th32: ( ultraset BL) = ( union X) & X is Subset of ( StoneR BL) implies ex Y be Element of ( Fin X) st ( ultraset BL) = ( union Y)

    proof

      assume that

       A1: ( ultraset BL) = ( union X) and

       A2: X is Subset of ( StoneR BL);

      assume

       A3: not thesis;

      consider Y be Element of ( Fin X) such that

       A4: Y is non empty by A1, Th27, ZFMISC_1: 2;



       A5: Y c= X by FINSUB_1:def 5;

      then

       A6: Y c= ( StoneR BL) by A2, XBOOLE_1: 1;

      set x = the Element of Y;



       A7: x in X by A4, A5;

      x in ( StoneR BL) by A4, A6;

      then

      consider b such that

       A8: x = (( UFilter BL) . b) by Th23;

      set CY = { (a ` ) : (( UFilter BL) . a) in X };

      consider c such that

       A9: c = (b ` );



       A10: c in CY by A7, A8, A9;

      CY c= the carrier of BL

      proof

        let x be object;

        assume x in CY;

        then ex b st (x = (b ` )) & ((( UFilter BL) . b) in X);

        hence thesis;

      end;

      then

      reconsider CY as non empty Subset of BL by A10;

      set H = <.CY.);

      for B be non empty Element of ( Fin the carrier of BL) st B c= CY holds ( FinMeet B) <> ( Bottom BL)

      proof

        let B be non empty Element of ( Fin the carrier of BL) such that

         A11: B c= CY and

         A12: ( FinMeet B) = ( Bottom BL);



         A13: B is Subset of BL by FINSUB_1: 16;



         A14: ( dom ( UFilter BL)) = the carrier of BL by FUNCT_2:def 1;

        (( UFilter BL) .: B) c= ( rng ( UFilter BL)) by RELAT_1: 111;

        then

        reconsider D = (( UFilter BL) .: B) as non empty Subset-Family of ( ultraset BL) by A13, A14, XBOOLE_1: 1;

         A15:

        now

          set x = the Element of (( UFilter BL) . ( Bottom BL));

          assume ( {} ( ultraset BL)) <> (( UFilter BL) . ( Bottom BL));

          then ex F st F = x & F is being_ultrafilter & ( Bottom BL) in F by Th17;

          hence contradiction by Th29;

        end;

        deffunc U( Subset of ( ultraset BL), Subset of ( ultraset BL)) = ($1 /\ $2);

        consider G be BinOp of ( bool ( ultraset BL)) such that

         A16: for x,y be Subset of ( ultraset BL) holds (G . (x,y)) = U(x,y) from BINOP_1:sch 4;



         A17: G is commutative

        proof

          let x,y be Subset of ( ultraset BL);

          (G . (x,y)) = (y /\ x) by A16

          .= (G . (y,x)) by A16;

          hence thesis;

        end;



         A18: G is associative

        proof

          let x,y,z be Subset of ( ultraset BL);

          (G . (x,(G . (y,z)))) = (G . (x,(y /\ z))) by A16

          .= (x /\ (y /\ z)) by A16

          .= ((x /\ y) /\ z) by XBOOLE_1: 16

          .= (G . ((x /\ y),z)) by A16

          .= (G . ((G . (x,y)),z)) by A16;

          hence thesis;

        end;



         A19: G is idempotent

        proof

          let x be Subset of ( ultraset BL);

          (G . (x,x)) = (x /\ x) by A16

          .= x;

          hence thesis;

        end;



         A20: for x,y be Element of BL holds (( UFilter BL) . (the L_meet of BL . (x,y))) = (G . ((( UFilter BL) . x),(( UFilter BL) . y)))

        proof

          let x,y be Element of BL;



          thus (( UFilter BL) . (the L_meet of BL . (x,y))) = (( UFilter BL) . (x "/\" y))

          .= ((( UFilter BL) . x) /\ (( UFilter BL) . y)) by Th20

          .= (G . ((( UFilter BL) . x),(( UFilter BL) . y))) by A16;

        end;

        reconsider DD = D as Element of ( Fin ( bool ( ultraset BL)));

        ( id BL) = ( id the carrier of BL);



        then

         A21: (( UFilter BL) . ( FinMeet B)) = (( UFilter BL) . ( FinMeet (B,( id the carrier of BL)))) by LATTICE4:def 9

        .= (( UFilter BL) . (the L_meet of BL $$ (B,( id the carrier of BL)))) by LATTICE2:def 4

        .= (G $$ (B,(( UFilter BL) * ( id the carrier of BL)))) by A17, A18, A19, A20, SETWISEO: 30

        .= (G $$ (B,( UFilter BL))) by FUNCT_2: 17

        .= (G $$ (B,(( id ( bool ( ultraset BL))) * ( UFilter BL)))) by FUNCT_2: 17

        .= (G $$ (DD,( id ( bool ( ultraset BL))))) by A17, A18, A19, SETWISEO: 29;

        defpred X[ Element of ( Fin ( bool ( ultraset BL)))] means for D be non empty Subset-Family of ( ultraset BL) st D = $1 holds (G $$ ($1,( id ( bool ( ultraset BL))))) = ( meet D);



         A22: X[( {}. ( bool ( ultraset BL)))];



         A23: for DD be Element of ( Fin ( bool ( ultraset BL))), b be Subset of ( ultraset BL) st X[DD] holds X[(DD \/ {.b.})]

        proof

          let DD be Element of ( Fin ( bool ( ultraset BL))), b be Subset of ( ultraset BL);

          assume

           A24: for D be non empty Subset-Family of ( ultraset BL) st D = DD holds (G $$ (DD,( id ( bool ( ultraset BL))))) = ( meet D);

          let D be non empty Subset-Family of ( ultraset BL) such that

           A25: D = (DD \/ {b});

          now

            per cases ;

              suppose

               A26: DD is empty;



              hence (G $$ ((DD \/ {.b.}),( id ( bool ( ultraset BL))))) = (( id ( bool ( ultraset BL))) . b) by A17, A18, SETWISEO: 17

              .= b

              .= ( meet D) by A25, A26, SETFAM_1: 10;

            end;

              suppose

               A27: DD is non empty;

              DD c= D by A25, XBOOLE_1: 7;

              then

              reconsider D1 = DD as non empty Subset-Family of ( ultraset BL) by A27, XBOOLE_1: 1;

              reconsider D1 as non empty Subset-Family of ( ultraset BL);



              thus (G $$ ((DD \/ {.b.}),( id ( bool ( ultraset BL))))) = (G . ((G $$ (DD,( id ( bool ( ultraset BL))))),(( id ( bool ( ultraset BL))) . b))) by A17, A18, A19, A27, SETWISEO: 20

              .= (G . ((G $$ (DD,( id ( bool ( ultraset BL))))),b))

              .= ((G $$ (DD,( id ( bool ( ultraset BL))))) /\ b) by A16

              .= (( meet D1) /\ b) by A24

              .= (( meet D1) /\ ( meet {b})) by SETFAM_1: 10

              .= ( meet D) by A25, SETFAM_1: 9;

            end;

          end;

          hence thesis;

        end;

        for DD be Element of ( Fin ( bool ( ultraset BL))) holds X[DD] from SETWISEO:sch 4( A22, A23);

        then ( meet D) = ( {} ( ultraset BL)) by A12, A15, A21;



        then

         A28: ( union ( COMPLEMENT D)) = (( [#] ( ultraset BL)) \ {} ) by SETFAM_1: 34

        .= ( ultraset BL);



         A29: ( COMPLEMENT D) c= X

        proof

          let x be object;

          assume

           A30: x in ( COMPLEMENT D);

          then

          reconsider c = x as Subset of ( ultraset BL);

          (c ` ) in D by A30, SETFAM_1:def 7;

          then

          consider a be object such that

           A31: a in ( dom ( UFilter BL)) and

           A32: a in B and

           A33: (c ` ) = (( UFilter BL) . a) by FUNCT_1:def 6;

          reconsider a as Element of BL by A31;

          a in CY by A11, A32;

          then ((a ` ) ` ) in CY;

          then

          consider b be Element of BL such that

           A34: (b ` ) = ((a ` ) ` ) and

           A35: (( UFilter BL) . b) in X;

          x = ((( UFilter BL) . a) ` ) by A33

          .= (( UFilter BL) . (a ` )) by Th25

          .= (( UFilter BL) . ((b ` ) ` )) by A34

          .= (( UFilter BL) . b);

          hence thesis by A35;

        end;

        ( COMPLEMENT D) is finite

        proof



           A36: D is finite;

          deffunc U( Subset of ( ultraset BL)) = ($1 ` );



           A37: { U(w) where w be Subset of ( ultraset BL) : w in D } is finite from FRAENKEL:sch 21( A36);

          { (w ` ) where w be Subset of ( ultraset BL) : w in D } = ( COMPLEMENT D)

          proof

            hereby

              let x be object;

              assume x in { (w ` ) where w be Subset of ( ultraset BL) : w in D };

              then

              consider w be Subset of ( ultraset BL) such that

               A38: (w ` ) = x and

               A39: w in D;

              ((w ` ) ` ) in D by A39;

              hence x in ( COMPLEMENT D) by A38, SETFAM_1:def 7;

            end;

            let x be object;

            assume

             A40: x in ( COMPLEMENT D);

            then

            reconsider x9 = x as Subset of ( ultraset BL);



             A41: (x9 ` ) in D by A40, SETFAM_1:def 7;

            ((x9 ` ) ` ) = x9;

            hence thesis by A41;

          end;

          hence thesis by A37;

        end;

        then ( COMPLEMENT D) is Element of ( Fin X) by A29, FINSUB_1:def 5;

        hence contradiction by A3, A28;

      end;

      then H <> the carrier of BL by Th28;

      then

      consider F such that

       A42: H c= F and

       A43: F is being_ultrafilter by FILTER_0: 18;



       A44: CY c= H by FILTER_0:def 4;

       not F in ( union X)

      proof

        assume F in ( union X);

        then

        consider Y be set such that

         A45: F in Y and

         A46: Y in X by TARSKI:def 4;

        consider a be object such that

         A47: a in ( dom ( UFilter BL)) and

         A48: Y = (( UFilter BL) . a) by A2, A46, FUNCT_1:def 3;

        reconsider a as Element of BL by A47;

        (a ` ) in CY by A46, A48;

        then

         A49: (a ` ) in H by A44;

        a in F by A45, A48, Th18;

        hence contradiction by A42, A43, A49, FILTER_0: 46;

      end;

      hence contradiction by A1, A43;

    end;



     Lm2: ( StoneR BL) c= ( OpenClosedSet ( StoneSpace BL))

    proof

      let x be object;

      assume

       A1: x in ( StoneR BL);

      then

      reconsider p = x as Subset of ( StoneSpace BL) by Def8;



       A2: p is open by A1, Lm1;

      p is closed

      proof

        set ST = ( StoneSpace BL);



         A3: ( [#] ST) = ( ultraset BL) by Def8;

        consider a such that

         A4: (( UFilter BL) . a) = p by A1, Th23;

        (p ` ) = (( UFilter BL) . (a ` )) by A3, A4, Th25;

        then (p ` ) in ( StoneR BL) by Th23;

        then (p ` ) is open by Lm1;

        hence thesis by TOPS_1: 3;

      end;

      hence thesis by A2;

    end;

    theorem :: LOPCLSET:33



     Th33: ( StoneR BL) = ( OpenClosedSet ( StoneSpace BL))

    proof



       A1: ( StoneR BL) c= ( OpenClosedSet ( StoneSpace BL)) by Lm2;

      ( OpenClosedSet ( StoneSpace BL)) c= ( StoneR BL)

      proof

        let x be object;

        assume

         A2: x in ( OpenClosedSet ( StoneSpace BL));

        then

        reconsider X = x as Subset of ( StoneSpace BL);



         A3: the topology of ( StoneSpace BL) = { ( union A) where A be Subset-Family of ( ultraset BL) : A c= ( StoneR BL) } by Def8;



         A4: X is open closed by A2, Th1, Th2;

        then

         A5: (X ` ) is open closed;

        X in the topology of ( StoneSpace BL) by A4, PRE_TOPC:def 2;

        then

        consider A1 be Subset-Family of ( ultraset BL) such that

         A6: X = ( union A1) and

         A7: A1 c= ( StoneR BL) by A3;

        (X ` ) in the topology of ( StoneSpace BL) by A5, PRE_TOPC:def 2;

        then

        consider A2 be Subset-Family of ( ultraset BL) such that

         A8: (X ` ) = ( union A2) and

         A9: A2 c= ( StoneR BL) by A3;



         A10: X is Subset of ( ultraset BL) by Def8;

        set AA = (A1 \/ A2);



         A11: ( ultraset BL) = ( [#] ( StoneSpace BL)) by Def8

        .= (X \/ (X ` )) by PRE_TOPC: 2

        .= ( union AA) by A6, A8, ZFMISC_1: 78;



         A12: AA c= ( StoneR BL) by A7, A9, XBOOLE_1: 8;

        then

        consider Y be Element of ( Fin AA) such that

         A13: ( ultraset BL) = ( union Y) by A11, Th32;



         A14: Y c= AA by FINSUB_1:def 5;

        then

         A15: Y c= ( StoneR BL) by A12;

        set D = (A1 /\ Y);



         A16: Y = (AA /\ Y) by A14, XBOOLE_1: 28

        .= (D \/ (A2 /\ Y)) by XBOOLE_1: 23;

        now

          let y be set;

          assume y in (A2 /\ Y);

          then y in A2 by XBOOLE_0:def 4;

          then

           A17: y c= (X ` ) by A8, ZFMISC_1: 74;

          (X ` ) misses X by XBOOLE_1: 79;

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

          then (y /\ X) = {} by A17, XBOOLE_1: 3, XBOOLE_1: 26;

          hence y misses X;

        end;

        then

         A18: X c= ( union D) by A10, A13, A16, SETFAM_1: 42;

        per cases ;

          suppose D = {} ;

          then

           A19: X = {} by A18, ZFMISC_1: 2;

           {} = (( UFilter BL) . ( Bottom BL)) by Th30;

          hence thesis by A19, FUNCT_2: 4;

        end;

          suppose

           A20: D <> {} ;



           A21: D c= Y by XBOOLE_1: 17;

          reconsider D as non empty Subset-Family of ( ultraset BL) by A20;

          reconsider D as non empty Subset-Family of ( ultraset BL);



           A22: ( union D) c= (( union A1) /\ ( union Y)) by ZFMISC_1: 79;

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

          then ( union D) c= X by A6, A22;

          then

           A23: X = ( union D) by A18;



           A24: D c= ( rng ( UFilter BL)) by A15, A21;



           A25: ( rng ( UFilter BL)) = ( dom ( id ( StoneR BL)));



           A26: ( dom ( UFilter BL)) = ( dom ( UFilter BL));

          ( UFilter BL) = (( id ( StoneR BL)) * ( UFilter BL)) by RELAT_1: 54;

          then (( UFilter BL),( id ( StoneR BL))) are_fiberwise_equipotent by A25, A26, CLASSES1: 77;



          then ( card (( UFilter BL) " D)) = ( card (( id ( StoneR BL)) " D)) by CLASSES1: 78

          .= ( card D) by A24, FUNCT_2: 94;

          then (( UFilter BL) " D) is finite;

          then

          reconsider B = (( UFilter BL) " D) as Element of ( Fin the carrier of BL) by FINSUB_1:def 5;



           A27: D = (( UFilter BL) .: B) by A15, A21, FUNCT_1: 77, XBOOLE_1: 1;

          then

           A28: B is non empty;

          deffunc U( Subset of ( ultraset BL), Subset of ( ultraset BL)) = ($1 \/ $2);

          consider G be BinOp of ( bool ( ultraset BL)) such that

           A29: for x,y be Subset of ( ultraset BL) holds (G . (x,y)) = U(x,y) from BINOP_1:sch 4;



           A30: G is commutative

          proof

            let x,y be Subset of ( ultraset BL);

            (G . (x,y)) = (y \/ x) by A29

            .= (G . (y,x)) by A29;

            hence thesis;

          end;



           A31: G is associative

          proof

            let x,y,z be Subset of ( ultraset BL);

            (G . (x,(G . (y,z)))) = (G . (x,(y \/ z))) by A29

            .= (x \/ (y \/ z)) by A29

            .= ((x \/ y) \/ z) by XBOOLE_1: 4

            .= (G . ((x \/ y),z)) by A29

            .= (G . ((G . (x,y)),z)) by A29;

            hence thesis;

          end;



           A32: G is idempotent

          proof

            let x be Subset of ( ultraset BL);

            (G . (x,x)) = (x \/ x) by A29

            .= x;

            hence thesis;

          end;



           A33: for x,y be Element of BL holds (( UFilter BL) . (the L_join of BL . (x,y))) = (G . ((( UFilter BL) . x),(( UFilter BL) . y)))

          proof

            let x,y be Element of BL;



            thus (( UFilter BL) . (the L_join of BL . (x,y))) = (( UFilter BL) . (x "\/" y))

            .= ((( UFilter BL) . x) \/ (( UFilter BL) . y)) by Th21

            .= (G . ((( UFilter BL) . x),(( UFilter BL) . y))) by A29;

          end;

          reconsider DD = D as Element of ( Fin ( bool ( ultraset BL))) by FINSUB_1:def 5;

          ( id BL) = ( id the carrier of BL);



          then

           A34: (( UFilter BL) . ( FinJoin B)) = (( UFilter BL) . ( FinJoin (B,( id the carrier of BL)))) by LATTICE4:def 8

          .= (( UFilter BL) . (the L_join of BL $$ (B,( id the carrier of BL)))) by LATTICE2:def 3

          .= (G $$ (B,(( UFilter BL) * ( id the carrier of BL)))) by A28, A30, A31, A32, A33, SETWISEO: 30

          .= (G $$ (B,( UFilter BL))) by FUNCT_2: 17

          .= (G $$ (B,(( id ( bool ( ultraset BL))) * ( UFilter BL)))) by FUNCT_2: 17

          .= (G $$ (DD,( id ( bool ( ultraset BL))))) by A27, A28, A30, A31, A32, SETWISEO: 29;

          defpred X[ Element of ( Fin ( bool ( ultraset BL)))] means for D be non empty Subset-Family of ( ultraset BL) st D = $1 holds (G $$ ($1,( id ( bool ( ultraset BL))))) = ( union D);



           A35: X[( {}. ( bool ( ultraset BL)))];



           A36: for DD be Element of ( Fin ( bool ( ultraset BL))), b be Subset of ( ultraset BL) st X[DD] holds X[(DD \/ {.b.})]

          proof

            let DD be Element of ( Fin ( bool ( ultraset BL))), b be Subset of ( ultraset BL);

            assume

             A37: for D be non empty Subset-Family of ( ultraset BL) st D = DD holds (G $$ (DD,( id ( bool ( ultraset BL))))) = ( union D);

            let D be non empty Subset-Family of ( ultraset BL) such that

             A38: D = (DD \/ {b});

            now

              per cases ;

                suppose

                 A39: DD is empty;



                hence (G $$ ((DD \/ {.b.}),( id ( bool ( ultraset BL))))) = (( id ( bool ( ultraset BL))) . b) by A30, A31, SETWISEO: 17

                .= b

                .= ( union D) by A38, A39, ZFMISC_1: 25;

              end;

                suppose

                 A40: DD is non empty;

                DD c= D by A38, XBOOLE_1: 7;

                then

                reconsider D1 = DD as non empty Subset-Family of ( ultraset BL) by A40, XBOOLE_1: 1;

                reconsider D1 as non empty Subset-Family of ( ultraset BL);



                thus (G $$ ((DD \/ {.b.}),( id ( bool ( ultraset BL))))) = (G . ((G $$ (DD,( id ( bool ( ultraset BL))))),(( id ( bool ( ultraset BL))) . b))) by A30, A31, A32, A40, SETWISEO: 20

                .= (G . ((G $$ (DD,( id ( bool ( ultraset BL))))),b))

                .= ((G $$ (DD,( id ( bool ( ultraset BL))))) \/ b) by A29

                .= (( union D1) \/ b) by A37

                .= (( union D1) \/ ( union {b})) by ZFMISC_1: 25

                .= ( union D) by A38, ZFMISC_1: 78;

              end;

            end;

            hence thesis;

          end;

          for DD be Element of ( Fin ( bool ( ultraset BL))) holds X[DD] from SETWISEO:sch 4( A35, A36);

          then (( UFilter BL) . ( FinJoin B)) = x by A23, A34;

          hence thesis by FUNCT_2: 4;

        end;

      end;

      hence thesis by A1;

    end;

    definition

      let BL;

      :: original: UFilter

      redefine

      func UFilter BL -> Homomorphism of BL, ( StoneBLattice BL) ;

      coherence

      proof

        reconsider g = ( UFilter BL) as Function of the carrier of BL, ( bool ( ultraset BL));

        set SL = ( StoneBLattice BL);

        ( rng g) = ( StoneR BL);

        then ( rng g) c= ( OpenClosedSet ( StoneSpace BL)) by Lm2;

        then

        reconsider f = ( UFilter BL) as Function of the carrier of BL, the carrier of SL by FUNCT_2: 6;

        now

          let p, q;



          thus (f . (p "\/" q)) = ((f . p) \/ (f . q)) by Th21

          .= ((f . p) "\/" (f . q)) by Def2;



          thus (f . (p "/\" q)) = ((f . p) /\ (f . q)) by Th20

          .= ((f . p) "/\" (f . q)) by Def3;

        end;

        then f is "\/"-preserving "/\"-preserving by LATTICE4:def 1, LATTICE4:def 2;

        hence thesis;

      end;

    end

    theorem :: LOPCLSET:34



     Th34: ( rng ( UFilter BL)) = the carrier of ( StoneBLattice BL)

    proof



      thus ( rng ( UFilter BL)) = ( StoneR BL)

      .= the carrier of ( StoneBLattice BL) by Th33;

    end;

    registration

      let BL;

      cluster ( UFilter BL) -> bijective;

      coherence

      proof

        ( rng ( UFilter BL)) = the carrier of ( StoneBLattice BL) by Th34;

        then ( UFilter BL) is onto by FUNCT_2:def 3;

        hence thesis;

      end;

    end

    theorem :: LOPCLSET:35



     Th35: (BL,( StoneBLattice BL)) are_isomorphic

    proof

      ex f be Homomorphism of BL, ( StoneBLattice BL) st f = ( UFilter BL) & f is bijective;

      hence thesis by LATTICE4:def 3;

    end;

    ::$Notion-Name

    theorem :: LOPCLSET:36

    for BL be non trivial B_Lattice holds ex T be non empty TopSpace st (BL,( OpenClosedSetLatt T)) are_isomorphic

    proof

      let BL be non trivial B_Lattice;

      reconsider T = ( StoneSpace BL) as non empty TopSpace;

      take T;

      ( OpenClosedSetLatt T) = ( StoneBLattice BL);

      hence thesis by Th35;

    end;