decomp_1.miz

    begin

    definition

      let T be TopStruct;

      :: DECOMP_1:def1

      mode alpha-set of T -> Subset of T means

      : Def1: it c= ( Int ( Cl ( Int it )));

      existence

      proof

        take ( {} T);

        thus thesis by XBOOLE_1: 2;

      end;

      let IT be Subset of T;

      :: DECOMP_1:def2

      attr IT is semi-open means IT c= ( Cl ( Int IT));

      :: DECOMP_1:def3

      attr IT is pre-open means IT c= ( Int ( Cl IT));

      :: DECOMP_1:def4

      attr IT is pre-semi-open means IT c= ( Cl ( Int ( Cl IT)));

      :: DECOMP_1:def5

      attr IT is semi-pre-open means IT c= (( Cl ( Int IT)) \/ ( Int ( Cl IT)));

    end

    definition

      let T be TopStruct;

      let B be Subset of T;

      :: DECOMP_1:def6

      func sInt B -> Subset of T equals (B /\ ( Cl ( Int B)));

      coherence ;

      :: DECOMP_1:def7

      func pInt B -> Subset of T equals (B /\ ( Int ( Cl B)));

      coherence ;

      :: DECOMP_1:def8

      func alphaInt B -> Subset of T equals (B /\ ( Int ( Cl ( Int B))));

      coherence ;

      :: DECOMP_1:def9

      func psInt B -> Subset of T equals (B /\ ( Cl ( Int ( Cl B))));

      coherence ;

    end

    definition

      let T be TopStruct;

      let B be Subset of T;

      :: DECOMP_1:def10

      func spInt B -> Subset of T equals (( sInt B) \/ ( pInt B));

      coherence ;

    end

    definition

      let T be TopSpace;

      :: DECOMP_1:def11

      func T ^alpha -> Subset-Family of T equals { B where B be Subset of T : B is alpha-set of T };

      coherence

      proof

        defpred P[ set] means $1 is alpha-set of T;

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def12

      func SO T -> Subset-Family of T equals { B where B be Subset of T : B is semi-open };

      coherence

      proof

        defpred P[ Subset of T] means $1 is semi-open;

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def13

      func PO T -> Subset-Family of T equals { B where B be Subset of T : B is pre-open };

      coherence

      proof

        defpred P[ Subset of T] means $1 is pre-open;

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def14

      func SPO T -> Subset-Family of T equals { B where B be Subset of T : B is semi-pre-open };

      coherence

      proof

        defpred P[ Subset of T] means $1 is semi-pre-open;

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def15

      func PSO T -> Subset-Family of T equals { B where B be Subset of T : B is pre-semi-open };

      coherence

      proof

        defpred P[ Subset of T] means $1 is pre-semi-open;

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def16

      func D(c,alpha) (T) -> Subset-Family of T equals { B where B be Subset of T : ( Int B) = ( alphaInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( Int $1) = ( alphaInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def17

      func D(c,p) (T) -> Subset-Family of T equals { B where B be Subset of T : ( Int B) = ( pInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( Int $1) = ( pInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def18

      func D(c,s) (T) -> Subset-Family of T equals { B where B be Subset of T : ( Int B) = ( sInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( Int $1) = ( sInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def19

      func D(c,ps) (T) -> Subset-Family of T equals { B where B be Subset of T : ( Int B) = ( psInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( Int $1) = ( psInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def20

      func D(alpha,p) (T) -> Subset-Family of T equals { B where B be Subset of T : ( alphaInt B) = ( pInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( alphaInt $1) = ( pInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def21

      func D(alpha,s) (T) -> Subset-Family of T equals { B where B be Subset of T : ( alphaInt B) = ( sInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( alphaInt $1) = ( sInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def22

      func D(alpha,ps) (T) -> Subset-Family of T equals { B where B be Subset of T : ( alphaInt B) = ( psInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( alphaInt $1) = ( psInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def23

      func D(p,sp) (T) -> Subset-Family of T equals { B where B be Subset of T : ( pInt B) = ( spInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( pInt $1) = ( spInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def24

      func D(p,ps) (T) -> Subset-Family of T equals { B where B be Subset of T : ( pInt B) = ( psInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( pInt $1) = ( psInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

      :: DECOMP_1:def25

      func D(sp,ps) (T) -> Subset-Family of T equals { B where B be Subset of T : ( spInt B) = ( psInt B) };

      coherence

      proof

        defpred P[ Subset of T] means ( spInt $1) = ( psInt $1);

        { B where B be Subset of T : P[B] } is Subset-Family of T from DOMAIN_1:sch 7;

        hence thesis;

      end;

    end

    reserve T for TopSpace,

B for Subset of T;

    theorem :: DECOMP_1:1



     Th1: ( alphaInt B) = ( pInt B) iff ( sInt B) = ( psInt B)

    proof

      hereby

        ( Cl ( Int B)) c= ( Cl B) by PRE_TOPC: 19, TOPS_1: 16;

        then ( Int ( Cl ( Int B))) c= ( Int ( Cl B)) by TOPS_1: 19;

        then ( Cl ( Int ( Cl ( Int B)))) c= ( Cl ( Int ( Cl B))) by PRE_TOPC: 19;

        then ( Cl ( Int B)) c= ( Cl ( Int ( Cl B))) by TOPS_1: 26;

        then

         A1: ( sInt B) c= (B /\ ( Cl ( Int ( Cl B)))) by XBOOLE_1: 26;

        assume ( alphaInt B) = ( pInt B);

        then ( Cl (B /\ ( Int ( Cl B)))) c= ( Cl ( Int ( Cl ( Int B)))) by PRE_TOPC: 19, XBOOLE_1: 17;

        then

         A2: ( Cl (B /\ ( Int ( Cl B)))) c= ( Cl ( Int B)) by TOPS_1: 26;

        ( Cl (B /\ ( Int ( Cl B)))) = ( Cl (( Cl B) /\ ( Int ( Cl B)))) by TOPS_1: 14;

        then ( Cl (B /\ ( Int ( Cl B)))) = ( Cl ( Int ( Cl B))) by TOPS_1: 16, XBOOLE_1: 28;

        then (B /\ ( Cl ( Int ( Cl B)))) c= (B /\ ( Cl ( Int B))) by A2, XBOOLE_1: 26;

        hence ( sInt B) = ( psInt B) by A1;

      end;



       A3: ( Int ( Cl B)) c= ( Cl ( Int ( Cl B))) by PRE_TOPC: 18;

      assume ( psInt B) = ( sInt B);

      then

       A4: ( psInt B) c= ( Cl ( Int B)) by XBOOLE_1: 17;

      (B /\ ( Int ( Cl B))) c= (B /\ ( Cl ( Int ( Cl B)))) by PRE_TOPC: 18, XBOOLE_1: 26;

      then (B /\ ( Int ( Cl B))) c= ( Cl ( Int B)) by A4;

      then

       A5: ( Cl (B /\ ( Int ( Cl B)))) c= ( Cl ( Cl ( Int B))) by PRE_TOPC: 19;

      ( Cl (B /\ ( Int ( Cl B)))) = ( Cl (( Cl B) /\ ( Int ( Cl B)))) by TOPS_1: 14;

      then ( Cl ( Int ( Cl B))) c= ( Cl ( Int B)) by A5, TOPS_1: 16, XBOOLE_1: 28;

      then ( Int ( Cl B)) c= ( Cl ( Int B)) by A3;

      then ( Int ( Int ( Cl B))) c= ( Int ( Cl ( Int B))) by TOPS_1: 19;

      then

       A6: (B /\ ( Int ( Cl B))) c= (B /\ ( Int ( Cl ( Int B)))) by XBOOLE_1: 26;

      ( Cl ( Int B)) c= ( Cl B) by PRE_TOPC: 19, TOPS_1: 16;

      then ( Int ( Cl ( Int B))) c= ( Int ( Cl B)) by TOPS_1: 19;

      then ( alphaInt B) c= (B /\ ( Int ( Cl B))) by XBOOLE_1: 26;

      hence thesis by A6;

    end;

    theorem :: DECOMP_1:2



     Th2: B is alpha-set of T iff B = ( alphaInt B) by Def1, XBOOLE_1: 17, XBOOLE_1: 28;

    theorem :: DECOMP_1:3



     Th3: B is semi-open iff B = ( sInt B) by XBOOLE_1: 17, XBOOLE_1: 28;

    theorem :: DECOMP_1:4



     Th4: B is pre-open iff B = ( pInt B) by XBOOLE_1: 17, XBOOLE_1: 28;

    theorem :: DECOMP_1:5



     Th5: B is pre-semi-open iff B = ( psInt B) by XBOOLE_1: 17, XBOOLE_1: 28;

    theorem :: DECOMP_1:6



     Th6: B is semi-pre-open iff B = ( spInt B)

    proof

      hereby

        assume B is semi-pre-open;

        then B = (B /\ (( Cl ( Int B)) \/ ( Int ( Cl B)))) by XBOOLE_1: 28;

        hence B = ( spInt B) by XBOOLE_1: 23;

      end;

      assume B = ( spInt B);

      then B = (B /\ (( Cl ( Int B)) \/ ( Int ( Cl B)))) by XBOOLE_1: 23;

      hence thesis by XBOOLE_1: 17;

    end;

    theorem :: DECOMP_1:7



     Th7: ((T ^alpha ) /\ ( D(c,alpha) T)) = the topology of T

    proof

      thus ((T ^alpha ) /\ ( D(c,alpha) T)) c= the topology of T

      proof

        let x be object;

        assume

         A1: x in ((T ^alpha ) /\ ( D(c,alpha) T));

        then x in (T ^alpha ) by XBOOLE_0:def 4;

        then

        consider A be Subset of T such that

         A2: x = A and

         A3: A is alpha-set of T;

        x in ( D(c,alpha) T) by A1, XBOOLE_0:def 4;

        then

        consider Z be Subset of T such that

         A4: x = Z and

         A5: ( Int Z) = ( alphaInt Z);

        A = ( alphaInt A) by A3, Th2;

        then Z is open by A2, A4, A5;

        hence thesis by A4, PRE_TOPC:def 2;

      end;

      let x be object;

      assume

       A6: x in the topology of T;

      then

      reconsider K = x as Subset of T;

      K is open by A6, PRE_TOPC:def 2;

      then

       A7: K = ( Int K) by TOPS_1: 23;

      then K c= ( Int ( Cl ( Int K))) by PRE_TOPC: 18, TOPS_1: 19;

      then

       A8: K is alpha-set of T by Def1;

      then ( Int K) = ( alphaInt K) by A7, Th2;

      then

       A9: K in { B : ( Int B) = ( alphaInt B) };

      K in (T ^alpha ) by A8;

      hence thesis by A9, XBOOLE_0:def 4;

    end;

    theorem :: DECOMP_1:8



     Th8: (( SO T) /\ ( D(c,s) T)) = the topology of T

    proof

      thus (( SO T) /\ ( D(c,s) T)) c= the topology of T

      proof

        let x be object;

        assume

         A1: x in (( SO T) /\ ( D(c,s) T));

        then x in ( SO T) by XBOOLE_0:def 4;

        then

        consider A be Subset of T such that

         A2: x = A and

         A3: A is semi-open;

        x in ( D(c,s) T) by A1, XBOOLE_0:def 4;

        then

        consider Z be Subset of T such that

         A4: x = Z and

         A5: ( Int Z) = ( sInt Z);

        A = ( sInt A) by A3, Th3;

        hence thesis by A4, PRE_TOPC:def 2, A2, A5;

      end;

      let x be object;

      assume

       A6: x in the topology of T;

      then

      reconsider K = x as Subset of T;

      K is open by A6, PRE_TOPC:def 2;

      then

       A7: K = ( Int K) by TOPS_1: 23;

      then

       A8: K is semi-open by PRE_TOPC: 18;

      then ( Int K) = ( sInt K) by A7, Th3;

      then

       A9: K in { B : ( Int B) = ( sInt B) };

      K in ( SO T) by A8;

      hence thesis by A9, XBOOLE_0:def 4;

    end;

    theorem :: DECOMP_1:9



     Th9: (( PO T) /\ ( D(c,p) T)) = the topology of T

    proof

      thus (( PO T) /\ ( D(c,p) T)) c= the topology of T

      proof

        let x be object;

        assume

         A1: x in (( PO T) /\ ( D(c,p) T));

        then x in ( PO T) by XBOOLE_0:def 4;

        then

        consider A be Subset of T such that

         A2: x = A and

         A3: A is pre-open;

        x in ( D(c,p) T) by A1, XBOOLE_0:def 4;

        then

        consider Z be Subset of T such that

         A4: x = Z and

         A5: ( Int Z) = ( pInt Z);

        A = ( pInt A) by A3, Th4;

        hence thesis by A4, PRE_TOPC:def 2, A2, A5;

      end;

      let x be object;

      assume

       A6: x in the topology of T;

      then

      reconsider K = x as Subset of T;

      K is open by A6, PRE_TOPC:def 2;

      then

       A7: K = ( Int K) by TOPS_1: 23;

      then

       A8: K is pre-open by PRE_TOPC: 18, TOPS_1: 19;

      then ( Int K) = ( pInt K) by A7, Th4;

      then

       A9: K in { B : ( Int B) = ( pInt B) };

      K in ( PO T) by A8;

      hence thesis by A9, XBOOLE_0:def 4;

    end;

    theorem :: DECOMP_1:10



     Th10: (( PSO T) /\ ( D(c,ps) T)) = the topology of T

    proof

      thus (( PSO T) /\ ( D(c,ps) T)) c= the topology of T

      proof

        let x be object;

        assume

         A1: x in (( PSO T) /\ ( D(c,ps) T));

        then x in ( PSO T) by XBOOLE_0:def 4;

        then

        consider A be Subset of T such that

         A2: x = A and

         A3: A is pre-semi-open;

        x in ( D(c,ps) T) by A1, XBOOLE_0:def 4;

        then

        consider Z be Subset of T such that

         A4: x = Z and

         A5: ( Int Z) = ( psInt Z);

        A = ( psInt A) by A3, Th5;

        hence thesis by A4, PRE_TOPC:def 2, A2, A5;

      end;

      let x be object;

      assume

       A6: x in the topology of T;

      then

      reconsider K = x as Subset of T;



       A7: ( Int ( Cl K)) c= ( Cl ( Int ( Cl K))) by PRE_TOPC: 18;

      K is open by A6, PRE_TOPC:def 2;

      then

       A8: K = ( Int K) by TOPS_1: 23;

      then K c= ( Int ( Cl K)) by PRE_TOPC: 18, TOPS_1: 19;

      then K c= ( Cl ( Int ( Cl K))) by A7;

      then

       A9: K is pre-semi-open;

      then ( Int K) = ( psInt K) by A8, Th5;

      then

       A10: K in { B : ( Int B) = ( psInt B) };

      K in ( PSO T) by A9;

      hence thesis by A10, XBOOLE_0:def 4;

    end;

    theorem :: DECOMP_1:11



     Th11: (( PO T) /\ ( D(alpha,p) T)) = (T ^alpha )

    proof

      thus (( PO T) /\ ( D(alpha,p) T)) c= (T ^alpha )

      proof

        let x be object;

        assume

         A1: x in (( PO T) /\ ( D(alpha,p) T));

        then x in ( PO T) by XBOOLE_0:def 4;

        then

        consider A be Subset of T such that

         A2: x = A and

         A3: A is pre-open;

        x in ( D(alpha,p) T) by A1, XBOOLE_0:def 4;

        then

        consider Z be Subset of T such that

         A4: x = Z and

         A5: ( alphaInt Z) = ( pInt Z);

        A = ( pInt A) by A3, Th4;

        then Z is alpha-set of T by A2, A4, A5, Th2;

        hence thesis by A4;

      end;

      let x be object;

      assume x in (T ^alpha );

      then

      consider K be Subset of T such that

       A6: x = K and

       A7: K is alpha-set of T;

      ( Cl ( Int K)) c= ( Cl K) by PRE_TOPC: 19, TOPS_1: 16;

      then

       A8: ( Int ( Cl ( Int K))) c= ( Int ( Cl K)) by TOPS_1: 19;

      K c= ( Int ( Cl ( Int K))) by A7, Def1;

      then K c= ( Int ( Cl K)) by A8;

      then

       A9: K is pre-open;

      then K = ( pInt K) by Th4;

      then ( alphaInt K) = ( pInt K) by A7, Th2;

      then

       A10: K in { B : ( alphaInt B) = ( pInt B) };

      K in ( PO T) by A9;

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

    end;

    theorem :: DECOMP_1:12



     Th12: (( SO T) /\ ( D(alpha,s) T)) = (T ^alpha )

    proof

      thus (( SO T) /\ ( D(alpha,s) T)) c= (T ^alpha )

      proof

        let x be object;

        assume

         A1: x in (( SO T) /\ ( D(alpha,s) T));

        then x in ( SO T) by XBOOLE_0:def 4;

        then

        consider A be Subset of T such that

         A2: x = A and

         A3: A is semi-open;

        x in ( D(alpha,s) T) by A1, XBOOLE_0:def 4;

        then

        consider Z be Subset of T such that

         A4: x = Z and

         A5: ( alphaInt Z) = ( sInt Z);

        Z is alpha-set of T by A2, A4, A5, Th2, A3, Th3;

        hence thesis by A4;

      end;

      let x be object;

      assume x in (T ^alpha );

      then

      consider K be Subset of T such that

       A6: x = K and

       A7: K is alpha-set of T;



       A8: ( Int ( Cl ( Int K))) c= ( Cl ( Int K)) by TOPS_1: 16;

      K c= ( Int ( Cl ( Int K))) by A7, Def1;

      then K c= ( Cl ( Int K)) by A8;

      then

       A9: K is semi-open;

      then K = ( sInt K) by Th3;

      then ( alphaInt K) = ( sInt K) by A7, Th2;

      then

       A10: K in { B : ( alphaInt B) = ( sInt B) };

      K in { B : B is semi-open } by A9;

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

    end;

    theorem :: DECOMP_1:13



     Th13: (( PSO T) /\ ( D(alpha,ps) T)) = (T ^alpha )

    proof

      thus (( PSO T) /\ ( D(alpha,ps) T)) c= (T ^alpha )

      proof

        let x be object;

        assume

         A1: x in (( PSO T) /\ ( D(alpha,ps) T));

        then x in ( PSO T) by XBOOLE_0:def 4;

        then

        consider A be Subset of T such that

         A2: x = A and

         A3: A is pre-semi-open;

        x in ( D(alpha,ps) T) by A1, XBOOLE_0:def 4;

        then

        consider Z be Subset of T such that

         A4: x = Z and

         A5: ( alphaInt Z) = ( psInt Z);

        A = ( psInt A) by A3, Th5;

        then Z is alpha-set of T by A2, A4, A5, Th2;

        hence thesis by A4;

      end;

      let x be object;

      assume x in (T ^alpha );

      then

      consider K be Subset of T such that

       A6: x = K and

       A7: K is alpha-set of T;

      ( Cl ( Int K)) c= ( Cl K) by PRE_TOPC: 19, TOPS_1: 16;

      then

       A8: ( Int ( Cl ( Int K))) c= ( Int ( Cl K)) by TOPS_1: 19;

      ( Int ( Cl K)) c= ( Cl ( Int ( Cl K))) by PRE_TOPC: 18;

      then

       A9: ( Int ( Cl ( Int K))) c= ( Cl ( Int ( Cl K))) by A8;

      K c= ( Int ( Cl ( Int K))) by A7, Def1;

      then K c= ( Cl ( Int ( Cl K))) by A9;

      then

       A10: K is pre-semi-open;

      then K = ( psInt K) by Th5;

      then ( alphaInt K) = ( psInt K) by A7, Th2;

      then

       A11: K in { B : ( alphaInt B) = ( psInt B) };

      K in ( PSO T) by A10;

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

    end;

    theorem :: DECOMP_1:14



     Th14: (( SPO T) /\ ( D(p,sp) T)) = ( PO T)

    proof

      thus (( SPO T) /\ ( D(p,sp) T)) c= ( PO T)

      proof

        let x be object;

        assume x in (( SPO T) /\ ( D(p,sp) T));

        then

         A0: x in ( SPO T) & x in ( D(p,sp) T) by XBOOLE_0:def 4;

        then

        consider B be Subset of T such that

         A1: x = B & B is semi-pre-open;



         A3: B = ( spInt B) by A1, Th6;

        consider B1 be Subset of T such that

         A2: x = B1 & ( pInt B1) = ( spInt B1) by A0;

        ( pInt B) = B by A2, A3, A1;

        then B is pre-open by Th4;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( PO T);

      then

      consider K be Subset of T such that

       A1: x = K and

       A2: K is pre-open;



       A3: ( Int ( Cl K)) c= (( Cl ( Int K)) \/ ( Int ( Cl K))) by XBOOLE_1: 7;

      K c= ( Int ( Cl K)) by A2;

      then K c= (( Cl ( Int K)) \/ ( Int ( Cl K))) by A3;

      then

       A4: K is semi-pre-open;

      then K = ( spInt K) by Th6;

      then ( pInt K) = ( spInt K) by A2, Th4;

      then

       A5: K in { B : ( pInt B) = ( spInt B) };

      K in ( SPO T) by A4;

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

    end;

    theorem :: DECOMP_1:15



     Th15: (( PSO T) /\ ( D(p,ps) T)) = ( PO T)

    proof

      thus (( PSO T) /\ ( D(p,ps) T)) c= ( PO T)

      proof

        let x be object;

        assume x in (( PSO T) /\ ( D(p,ps) T));

        then

         A0: x in ( PSO T) & x in ( D(p,ps) T) by XBOOLE_0:def 4;

        then

        consider B be Subset of T such that

         A1: x = B & B is pre-semi-open;



         A3: B = ( psInt B) by A1, Th5;

        consider B1 be Subset of T such that

         A2: x = B1 & ( pInt B1) = ( psInt B1) by A0;

        ( pInt B) = B by A2, A3, A1;

        then B is pre-open by Th4;

        then x in { B where B be Subset of T : B is pre-open } by A1;

        hence thesis;

      end;

      let x be object;

      assume x in ( PO T);

      then

      consider K be Subset of T such that

       A1: x = K and

       A2: K is pre-open;

      ( Int ( Cl K)) c= ( Cl ( Int ( Cl K))) by PRE_TOPC: 18;

      then K c= ( Cl ( Int ( Cl K))) by A2;

      then

       A4: K is pre-semi-open;

      then K = ( psInt K) by Th5;

      then ( pInt K) = ( psInt K) by A2, Th4;

      then

       A5: K in { B : ( pInt B) = ( psInt B) };

      K in ( PSO T) by A4;

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

    end;

    theorem :: DECOMP_1:16



     Th16: (( PSO T) /\ ( D(alpha,p) T)) = ( SO T)

    proof

      thus (( PSO T) /\ ( D(alpha,p) T)) c= ( SO T)

      proof

        let x be object;

        assume x in (( PSO T) /\ ( D(alpha,p) T));

        then

         A0: x in ( PSO T) & x in ( D(alpha,p) T) by XBOOLE_0:def 4;

        then

        consider B be Subset of T such that

         A1: x = B & B is pre-semi-open;



         A3: B = ( psInt B) by A1, Th5;

        consider B1 be Subset of T such that

         A2: x = B1 & ( alphaInt B1) = ( pInt B1) by A0;

        ( sInt B) = ( psInt B) by A2, A1, Th1;

        then ( sInt B) = B by A3;

        then B is semi-open by Th3;

        then x in ( SO T) by A1;

        hence thesis;

      end;

      let x be object;

      assume x in ( SO T);

      then

      consider K be Subset of T such that

       A1: x = K and

       A2: K is semi-open;

      ( Cl ( Int K)) c= ( Cl K) by PRE_TOPC: 19, TOPS_1: 16;

      then ( Int ( Cl ( Int K))) c= ( Int ( Cl K)) by TOPS_1: 19;

      then ( Cl ( Int ( Cl ( Int K)))) c= ( Cl ( Int ( Cl K))) by PRE_TOPC: 19;

      then ( Cl ( Int K)) c= ( Cl ( Int ( Cl K))) by TOPS_1: 26;

      then K c= ( Cl ( Int ( Cl K))) by A2;

      then

       A4: K is pre-semi-open;

      then K = ( psInt K) by Th5;

      then ( sInt K) = ( psInt K) by A2, Th3;

      then ( alphaInt K) = ( pInt K) by Th1;

      then

       A5: K in { B : ( alphaInt B) = ( pInt B) };

      K in ( PSO T) by A4;

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

    end;

    theorem :: DECOMP_1:17



     Th17: (( PSO T) /\ ( D(sp,ps) T)) = ( SPO T)

    proof

      thus (( PSO T) /\ ( D(sp,ps) T)) c= ( SPO T)

      proof

        let x be object;

        assume x in (( PSO T) /\ ( D(sp,ps) T));

        then

         A0: x in ( PSO T) & x in ( D(sp,ps) T) by XBOOLE_0:def 4;

        then

        consider B be Subset of T such that

         A1: x = B & B is pre-semi-open;



         A3: B = ( psInt B) by A1, Th5;

        consider B1 be Subset of T such that

         A2: x = B1 & ( spInt B1) = ( psInt B1) by A0;

        B is semi-pre-open by A1, A2, A3, Th6;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( SPO T);

      then

      consider K be Subset of T such that

       A1: x = K and

       A2: K is semi-pre-open;

      ( Cl ( Int K)) c= ( Cl K) by PRE_TOPC: 19, TOPS_1: 16;

      then ( Int ( Cl ( Int K))) c= ( Int ( Cl K)) by TOPS_1: 19;

      then ( Cl ( Int ( Cl ( Int K)))) c= ( Cl ( Int ( Cl K))) by PRE_TOPC: 19;

      then

       A3: ( Cl ( Int K)) c= ( Cl ( Int ( Cl K))) by TOPS_1: 26;

      ( Int ( Cl K)) c= ( Cl ( Int ( Cl K))) by PRE_TOPC: 18;

      then (( Cl ( Int K)) \/ ( Int ( Cl K))) c= ( Cl ( Int ( Cl K))) by A3, XBOOLE_1: 8;

      then K c= ( Cl ( Int ( Cl K))) by A2;

      then

       A5: K is pre-semi-open;

      then K = ( psInt K) by Th5;

      then ( spInt K) = ( psInt K) by A2, Th6;

      then

       A6: K in { B : ( spInt B) = ( psInt B) };

      K in ( PSO T) by A5;

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

    end;

    definition

      let X,Y be non empty TopSpace;

      let f be Function of X, Y;

      :: DECOMP_1:def26

      attr f is s-continuous means for G be Subset of Y st G is open holds (f " G) in ( SO X);

      :: DECOMP_1:def27

      attr f is p-continuous means for G be Subset of Y st G is open holds (f " G) in ( PO X);

      :: DECOMP_1:def28

      attr f is alpha-continuous means for G be Subset of Y st G is open holds (f " G) in (X ^alpha );

      :: DECOMP_1:def29

      attr f is ps-continuous means for G be Subset of Y st G is open holds (f " G) in ( PSO X);

      :: DECOMP_1:def30

      attr f is sp-continuous means for G be Subset of Y st G is open holds (f " G) in ( SPO X);

      :: DECOMP_1:def31

      attr f is (c,alpha)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(c,alpha) X);

      :: DECOMP_1:def32

      attr f is (c,s)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(c,s) X);

      :: DECOMP_1:def33

      attr f is (c,p)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(c,p) X);

      :: DECOMP_1:def34

      attr f is (c,ps)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(c,ps) X);

      :: DECOMP_1:def35

      attr f is (alpha,p)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(alpha,p) X);

      :: DECOMP_1:def36

      attr f is (alpha,s)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(alpha,s) X);

      :: DECOMP_1:def37

      attr f is (alpha,ps)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(alpha,ps) X);

      :: DECOMP_1:def38

      attr f is (p,ps)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(p,ps) X);

      :: DECOMP_1:def39

      attr f is (p,sp)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(p,sp) X);

      :: DECOMP_1:def40

      attr f is (sp,ps)-continuous means for G be Subset of Y st G is open holds (f " G) in ( D(sp,ps) X);

    end

    reserve X,Y for non empty TopSpace;

    reserve f for Function of X, Y;

    theorem :: DECOMP_1:18

    f is alpha-continuous iff f is p-continuous (alpha,p)-continuous

    proof

      hereby

        assume

         A1: f is alpha-continuous;

        thus f is p-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) in (X ^alpha ) by A1;

          then (f " V) in (( PO X) /\ ( D(alpha,p) X)) by Th11;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus f is (alpha,p)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) in (X ^alpha ) by A1;

          then (f " G) in (( PO X) /\ ( D(alpha,p) X)) by Th11;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A2: f is p-continuous (alpha,p)-continuous;

      let V be Subset of Y;

      assume V is open;

      then (f " V) in ( PO X) & (f " V) in ( D(alpha,p) X) by A2;

      then (f " V) in (( PO X) /\ ( D(alpha,p) X)) by XBOOLE_0:def 4;

      hence thesis by Th11;

    end;

    theorem :: DECOMP_1:19

    f is alpha-continuous iff f is s-continuous (alpha,s)-continuous

    proof

      hereby

        assume

         A1: f is alpha-continuous;

        thus f is s-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) in (X ^alpha ) by A1;

          then (f " V) in (( SO X) /\ ( D(alpha,s) X)) by Th12;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus f is (alpha,s)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) in (X ^alpha ) by A1;

          then (f " G) in (( SO X) /\ ( D(alpha,s) X)) by Th12;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A2: f is s-continuous (alpha,s)-continuous;

      let V be Subset of Y;

      assume V is open;

      then (f " V) in ( SO X) & (f " V) in ( D(alpha,s) X) by A2;

      then (f " V) in (( SO X) /\ ( D(alpha,s) X)) by XBOOLE_0:def 4;

      hence thesis by Th12;

    end;

    theorem :: DECOMP_1:20

    f is alpha-continuous iff f is ps-continuous (alpha,ps)-continuous

    proof

      hereby

        assume

         A1: f is alpha-continuous;

        thus f is ps-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) in (X ^alpha ) by A1;

          then (f " V) in (( PSO X) /\ ( D(alpha,ps) X)) by Th13;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus f is (alpha,ps)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) in (X ^alpha ) by A1;

          then (f " G) in (( PSO X) /\ ( D(alpha,ps) X)) by Th13;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A2: f is ps-continuous (alpha,ps)-continuous;

      let V be Subset of Y;

      assume V is open;

      then (f " V) in ( PSO X) & (f " V) in ( D(alpha,ps) X) by A2;

      then (f " V) in (( PSO X) /\ ( D(alpha,ps) X)) by XBOOLE_0:def 4;

      hence thesis by Th13;

    end;

    theorem :: DECOMP_1:21

    f is p-continuous iff f is sp-continuous (p,sp)-continuous

    proof

      hereby

        assume

         A1: f is p-continuous;

        thus f is sp-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) in ( PO X) by A1;

          then (f " V) in (( SPO X) /\ ( D(p,sp) X)) by Th14;

          hence (f " V) in ( SPO X) by XBOOLE_0:def 4;

        end;

        thus f is (p,sp)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) in ( PO X) by A1;

          then (f " G) in (( SPO X) /\ ( D(p,sp) X)) by Th14;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A2: f is sp-continuous (p,sp)-continuous;

      let V be Subset of Y;

      assume V is open;

      then (f " V) in ( SPO X) & (f " V) in ( D(p,sp) X) by A2;

      then (f " V) in (( SPO X) /\ ( D(p,sp) X)) by XBOOLE_0:def 4;

      hence thesis by Th14;

    end;

    theorem :: DECOMP_1:22

    f is p-continuous iff f is ps-continuous (p,ps)-continuous

    proof

      hereby

        assume

         A1: f is p-continuous;

        thus f is ps-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) in ( PO X) by A1;

          then (f " V) in (( PSO X) /\ ( D(p,ps) X)) by Th15;

          hence (f " V) in ( PSO X) by XBOOLE_0:def 4;

        end;

        thus f is (p,ps)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) in ( PO X) by A1;

          then (f " G) in (( PSO X) /\ ( D(p,ps) X)) by Th15;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A2: f is ps-continuous (p,ps)-continuous;

      let V be Subset of Y;

      assume V is open;

      then (f " V) in ( PSO X) & (f " V) in ( D(p,ps) X) by A2;

      then (f " V) in (( PSO X) /\ ( D(p,ps) X)) by XBOOLE_0:def 4;

      hence thesis by Th15;

    end;

    theorem :: DECOMP_1:23

    f is s-continuous iff f is ps-continuous (alpha,p)-continuous

    proof

      hereby

        assume

         A1: f is s-continuous;

        thus f is ps-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) in ( SO X) by A1;

          then (f " V) in (( PSO X) /\ ( D(alpha,p) X)) by Th16;

          hence (f " V) in ( PSO X) by XBOOLE_0:def 4;

        end;

        thus f is (alpha,p)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) in ( SO X) by A1;

          then (f " G) in (( PSO X) /\ ( D(alpha,p) X)) by Th16;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A2: f is ps-continuous (alpha,p)-continuous;

      let V be Subset of Y;

      assume V is open;

      then (f " V) in ( PSO X) & (f " V) in ( D(alpha,p) X) by A2;

      then (f " V) in (( PSO X) /\ ( D(alpha,p) X)) by XBOOLE_0:def 4;

      hence thesis by Th16;

    end;

    theorem :: DECOMP_1:24

    f is sp-continuous iff f is ps-continuous (sp,ps)-continuous

    proof

      hereby

        assume

         A1: f is sp-continuous;

        thus f is ps-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) in ( SPO X) by A1;

          then (f " V) in (( PSO X) /\ ( D(sp,ps) X)) by Th17;

          hence (f " V) in ( PSO X) by XBOOLE_0:def 4;

        end;

        thus f is (sp,ps)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) in ( SPO X) by A1;

          then (f " G) in (( PSO X) /\ ( D(sp,ps) X)) by Th17;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A2: f is ps-continuous (sp,ps)-continuous;

      let V be Subset of Y;

      assume V is open;

      then (f " V) in ( PSO X) & (f " V) in ( D(sp,ps) X) by A2;

      then (f " V) in (( PSO X) /\ ( D(sp,ps) X)) by XBOOLE_0:def 4;

      hence thesis by Th17;

    end;

    theorem :: DECOMP_1:25

    f is continuous iff f is alpha-continuous (c,alpha)-continuous

    proof



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

      hereby

        assume

         A2: f is continuous;

        thus f is alpha-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) is open by A1, A2, TOPS_2: 43;

          then (f " V) in the topology of X by PRE_TOPC:def 2;

          then (f " V) in ((X ^alpha ) /\ ( D(c,alpha) X)) by Th7;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus f is (c,alpha)-continuous

        proof

          let G be Subset of Y;

          assume G is open;

          then (f " G) is open by A1, A2, TOPS_2: 43;

          then (f " G) in the topology of X by PRE_TOPC:def 2;

          then (f " G) in ((X ^alpha ) /\ ( D(c,alpha) X)) by Th7;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A3: f is alpha-continuous (c,alpha)-continuous;

      now

        let V be Subset of Y;

        assume V is open;

        then (f " V) in (X ^alpha ) & (f " V) in ( D(c,alpha) X) by A3;

        then (f " V) in ((X ^alpha ) /\ ( D(c,alpha) X)) by XBOOLE_0:def 4;

        then (f " V) in the topology of X by Th7;

        hence (f " V) is open by PRE_TOPC:def 2;

      end;

      hence thesis by A1, TOPS_2: 43;

    end;

    theorem :: DECOMP_1:26

    f is continuous iff f is s-continuous (c,s)-continuous

    proof



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

      hereby

        assume

         A2: f is continuous;

        thus f is s-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) is open by A1, A2, TOPS_2: 43;

          then (f " V) in the topology of X by PRE_TOPC:def 2;

          then (f " V) in (( SO X) /\ ( D(c,s) X)) by Th8;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus f is (c,s)-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) is open by A1, A2, TOPS_2: 43;

          then (f " V) in the topology of X by PRE_TOPC:def 2;

          then (f " V) in (( SO X) /\ ( D(c,s) X)) by Th8;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A3: f is s-continuous (c,s)-continuous;

      now

        let V be Subset of Y;

        assume V is open;

        then (f " V) in ( SO X) & (f " V) in ( D(c,s) X) by A3;

        then (f " V) in (( SO X) /\ ( D(c,s) X)) by XBOOLE_0:def 4;

        then (f " V) in the topology of X by Th8;

        hence (f " V) is open by PRE_TOPC:def 2;

      end;

      hence thesis by A1, TOPS_2: 43;

    end;

    theorem :: DECOMP_1:27

    f is continuous iff f is p-continuous (c,p)-continuous

    proof



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

      hereby

        assume

         A2: f is continuous;

        thus f is p-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) is open by A1, A2, TOPS_2: 43;

          then (f " V) in the topology of X by PRE_TOPC:def 2;

          then (f " V) in (( PO X) /\ ( D(c,p) X)) by Th9;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus f is (c,p)-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) is open by A1, A2, TOPS_2: 43;

          then (f " V) in the topology of X by PRE_TOPC:def 2;

          then (f " V) in (( PO X) /\ ( D(c,p) X)) by Th9;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A3: f is p-continuous (c,p)-continuous;

      now

        let V be Subset of Y;

        assume V is open;

        then (f " V) in ( PO X) & (f " V) in ( D(c,p) X) by A3;

        then (f " V) in (( PO X) /\ ( D(c,p) X)) by XBOOLE_0:def 4;

        then (f " V) in the topology of X by Th9;

        hence (f " V) is open by PRE_TOPC:def 2;

      end;

      hence thesis by A1, TOPS_2: 43;

    end;

    theorem :: DECOMP_1:28

    f is continuous iff f is ps-continuous (c,ps)-continuous

    proof



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

      hereby

        assume

         A2: f is continuous;

        thus f is ps-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) is open by A1, A2, TOPS_2: 43;

          then (f " V) in the topology of X by PRE_TOPC:def 2;

          then (f " V) in (( PSO X) /\ ( D(c,ps) X)) by Th10;

          hence thesis by XBOOLE_0:def 4;

        end;

        thus f is (c,ps)-continuous

        proof

          let V be Subset of Y;

          assume V is open;

          then (f " V) is open by A1, A2, TOPS_2: 43;

          then (f " V) in the topology of X by PRE_TOPC:def 2;

          then (f " V) in (( PSO X) /\ ( D(c,ps) X)) by Th10;

          hence thesis by XBOOLE_0:def 4;

        end;

      end;

      assume

       A3: f is ps-continuous (c,ps)-continuous;

      now

        let V be Subset of Y;

        assume V is open;

        then (f " V) in ( PSO X) & (f " V) in ( D(c,ps) X) by A3;

        then (f " V) in (( PSO X) /\ ( D(c,ps) X)) by XBOOLE_0:def 4;

        then (f " V) in the topology of X by Th10;

        hence (f " V) is open by PRE_TOPC:def 2;

      end;

      hence thesis by A1, TOPS_2: 43;

    end;