:: DECOMP_1 semantic presentation begin definition let T be TopStruct ; mode alpha-set of T -> Subset of T means :Def1: :: DECOMP_1:def 1 it c= Int (Cl (Int it)); existence ex b1 being Subset of T st b1 c= Int (Cl (Int b1)) proof take {} T ; ::_thesis: {} T c= Int (Cl (Int ({} T))) thus {} T c= Int (Cl (Int ({} T))) by XBOOLE_1:2; ::_thesis: verum end; let IT be Subset of T; attrIT is semi-open means :Def2: :: DECOMP_1:def 2 IT c= Cl (Int IT); attrIT is pre-open means :Def3: :: DECOMP_1:def 3 IT c= Int (Cl IT); attrIT is pre-semi-open means :Def4: :: DECOMP_1:def 4 IT c= Cl (Int (Cl IT)); attrIT is semi-pre-open means :Def5: :: DECOMP_1:def 5 IT c= (Cl (Int IT)) \/ (Int (Cl IT)); end; :: deftheorem Def1 defines alpha-set DECOMP_1:def_1_:_ for T being TopStruct for b2 being Subset of T holds ( b2 is alpha-set of T iff b2 c= Int (Cl (Int b2)) ); :: deftheorem Def2 defines semi-open DECOMP_1:def_2_:_ for T being TopStruct for IT being Subset of T holds ( IT is semi-open iff IT c= Cl (Int IT) ); :: deftheorem Def3 defines pre-open DECOMP_1:def_3_:_ for T being TopStruct for IT being Subset of T holds ( IT is pre-open iff IT c= Int (Cl IT) ); :: deftheorem Def4 defines pre-semi-open DECOMP_1:def_4_:_ for T being TopStruct for IT being Subset of T holds ( IT is pre-semi-open iff IT c= Cl (Int (Cl IT)) ); :: deftheorem Def5 defines semi-pre-open DECOMP_1:def_5_:_ for T being TopStruct for IT being Subset of T holds ( IT is semi-pre-open iff IT c= (Cl (Int IT)) \/ (Int (Cl IT)) ); definition let T be TopStruct ; let B be Subset of T; func sInt B -> Subset of T equals :: DECOMP_1:def 6 B /\ (Cl (Int B)); coherence B /\ (Cl (Int B)) is Subset of T ; func pInt B -> Subset of T equals :: DECOMP_1:def 7 B /\ (Int (Cl B)); coherence B /\ (Int (Cl B)) is Subset of T ; func alphaInt B -> Subset of T equals :: DECOMP_1:def 8 B /\ (Int (Cl (Int B))); coherence B /\ (Int (Cl (Int B))) is Subset of T ; func psInt B -> Subset of T equals :: DECOMP_1:def 9 B /\ (Cl (Int (Cl B))); coherence B /\ (Cl (Int (Cl B))) is Subset of T ; end; :: deftheorem defines sInt DECOMP_1:def_6_:_ for T being TopStruct for B being Subset of T holds sInt B = B /\ (Cl (Int B)); :: deftheorem defines pInt DECOMP_1:def_7_:_ for T being TopStruct for B being Subset of T holds pInt B = B /\ (Int (Cl B)); :: deftheorem defines alphaInt DECOMP_1:def_8_:_ for T being TopStruct for B being Subset of T holds alphaInt B = B /\ (Int (Cl (Int B))); :: deftheorem defines psInt DECOMP_1:def_9_:_ for T being TopStruct for B being Subset of T holds psInt B = B /\ (Cl (Int (Cl B))); definition let T be TopStruct ; let B be Subset of T; func spInt B -> Subset of T equals :: DECOMP_1:def 10 (sInt B) \/ (pInt B); coherence (sInt B) \/ (pInt B) is Subset of T ; end; :: deftheorem defines spInt DECOMP_1:def_10_:_ for T being TopStruct for B being Subset of T holds spInt B = (sInt B) \/ (pInt B); definition let T be TopSpace; funcT ^alpha -> Subset-Family of T equals :: DECOMP_1:def 11 { B where B is Subset of T : B is alpha-set of T } ; coherence { B where B is Subset of T : B is alpha-set of T } is Subset-Family of T proof defpred S1[ set ] means \$1 is alpha-set of T; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : B is alpha-set of T } is Subset-Family of T ; ::_thesis: verum end; func SO T -> Subset-Family of T equals :: DECOMP_1:def 12 { B where B is Subset of T : B is semi-open } ; coherence { B where B is Subset of T : B is semi-open } is Subset-Family of T proof defpred S1[ Subset of T] means \$1 is semi-open ; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : B is semi-open } is Subset-Family of T ; ::_thesis: verum end; func PO T -> Subset-Family of T equals :: DECOMP_1:def 13 { B where B is Subset of T : B is pre-open } ; coherence { B where B is Subset of T : B is pre-open } is Subset-Family of T proof defpred S1[ Subset of T] means \$1 is pre-open ; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : B is pre-open } is Subset-Family of T ; ::_thesis: verum end; func SPO T -> Subset-Family of T equals :: DECOMP_1:def 14 { B where B is Subset of T : B is semi-pre-open } ; coherence { B where B is Subset of T : B is semi-pre-open } is Subset-Family of T proof defpred S1[ Subset of T] means \$1 is semi-pre-open ; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : B is semi-pre-open } is Subset-Family of T ; ::_thesis: verum end; func PSO T -> Subset-Family of T equals :: DECOMP_1:def 15 { B where B is Subset of T : B is pre-semi-open } ; coherence { B where B is Subset of T : B is pre-semi-open } is Subset-Family of T proof defpred S1[ Subset of T] means \$1 is pre-semi-open ; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : B is pre-semi-open } is Subset-Family of T ; ::_thesis: verum end; func D(c,alpha) T -> Subset-Family of T equals :: DECOMP_1:def 16 { B where B is Subset of T : Int B = alphaInt B } ; coherence { B where B is Subset of T : Int B = alphaInt B } is Subset-Family of T proof defpred S1[ Subset of T] means Int \$1 = alphaInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : Int B = alphaInt B } is Subset-Family of T ; ::_thesis: verum end; func D(c,p) T -> Subset-Family of T equals :: DECOMP_1:def 17 { B where B is Subset of T : Int B = pInt B } ; coherence { B where B is Subset of T : Int B = pInt B } is Subset-Family of T proof defpred S1[ Subset of T] means Int \$1 = pInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : Int B = pInt B } is Subset-Family of T ; ::_thesis: verum end; func D(c,s) T -> Subset-Family of T equals :: DECOMP_1:def 18 { B where B is Subset of T : Int B = sInt B } ; coherence { B where B is Subset of T : Int B = sInt B } is Subset-Family of T proof defpred S1[ Subset of T] means Int \$1 = sInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : Int B = sInt B } is Subset-Family of T ; ::_thesis: verum end; func D(c,ps) T -> Subset-Family of T equals :: DECOMP_1:def 19 { B where B is Subset of T : Int B = psInt B } ; coherence { B where B is Subset of T : Int B = psInt B } is Subset-Family of T proof defpred S1[ Subset of T] means Int \$1 = psInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : Int B = psInt B } is Subset-Family of T ; ::_thesis: verum end; func D(alpha,p) T -> Subset-Family of T equals :: DECOMP_1:def 20 { B where B is Subset of T : alphaInt B = pInt B } ; coherence { B where B is Subset of T : alphaInt B = pInt B } is Subset-Family of T proof defpred S1[ Subset of T] means alphaInt \$1 = pInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : alphaInt B = pInt B } is Subset-Family of T ; ::_thesis: verum end; func D(alpha,s) T -> Subset-Family of T equals :: DECOMP_1:def 21 { B where B is Subset of T : alphaInt B = sInt B } ; coherence { B where B is Subset of T : alphaInt B = sInt B } is Subset-Family of T proof defpred S1[ Subset of T] means alphaInt \$1 = sInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : alphaInt B = sInt B } is Subset-Family of T ; ::_thesis: verum end; func D(alpha,ps) T -> Subset-Family of T equals :: DECOMP_1:def 22 { B where B is Subset of T : alphaInt B = psInt B } ; coherence { B where B is Subset of T : alphaInt B = psInt B } is Subset-Family of T proof defpred S1[ Subset of T] means alphaInt \$1 = psInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : alphaInt B = psInt B } is Subset-Family of T ; ::_thesis: verum end; func D(p,sp) T -> Subset-Family of T equals :: DECOMP_1:def 23 { B where B is Subset of T : pInt B = spInt B } ; coherence { B where B is Subset of T : pInt B = spInt B } is Subset-Family of T proof defpred S1[ Subset of T] means pInt \$1 = spInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : pInt B = spInt B } is Subset-Family of T ; ::_thesis: verum end; func D(p,ps) T -> Subset-Family of T equals :: DECOMP_1:def 24 { B where B is Subset of T : pInt B = psInt B } ; coherence { B where B is Subset of T : pInt B = psInt B } is Subset-Family of T proof defpred S1[ Subset of T] means pInt \$1 = psInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : pInt B = psInt B } is Subset-Family of T ; ::_thesis: verum end; func D(sp,ps) T -> Subset-Family of T equals :: DECOMP_1:def 25 { B where B is Subset of T : spInt B = psInt B } ; coherence { B where B is Subset of T : spInt B = psInt B } is Subset-Family of T proof defpred S1[ Subset of T] means spInt \$1 = psInt \$1; { B where B is Subset of T : S1[B] } is Subset-Family of T from DOMAIN_1:sch_7(); hence { B where B is Subset of T : spInt B = psInt B } is Subset-Family of T ; ::_thesis: verum end; end; :: deftheorem defines ^alpha DECOMP_1:def_11_:_ for T being TopSpace holds T ^alpha = { B where B is Subset of T : B is alpha-set of T } ; :: deftheorem defines SO DECOMP_1:def_12_:_ for T being TopSpace holds SO T = { B where B is Subset of T : B is semi-open } ; :: deftheorem defines PO DECOMP_1:def_13_:_ for T being TopSpace holds PO T = { B where B is Subset of T : B is pre-open } ; :: deftheorem defines SPO DECOMP_1:def_14_:_ for T being TopSpace holds SPO T = { B where B is Subset of T : B is semi-pre-open } ; :: deftheorem defines PSO DECOMP_1:def_15_:_ for T being TopSpace holds PSO T = { B where B is Subset of T : B is pre-semi-open } ; :: deftheorem defines D(c,alpha) DECOMP_1:def_16_:_ for T being TopSpace holds D(c,alpha) T = { B where B is Subset of T : Int B = alphaInt B } ; :: deftheorem defines D(c,p) DECOMP_1:def_17_:_ for T being TopSpace holds D(c,p) T = { B where B is Subset of T : Int B = pInt B } ; :: deftheorem defines D(c,s) DECOMP_1:def_18_:_ for T being TopSpace holds D(c,s) T = { B where B is Subset of T : Int B = sInt B } ; :: deftheorem defines D(c,ps) DECOMP_1:def_19_:_ for T being TopSpace holds D(c,ps) T = { B where B is Subset of T : Int B = psInt B } ; :: deftheorem defines D(alpha,p) DECOMP_1:def_20_:_ for T being TopSpace holds D(alpha,p) T = { B where B is Subset of T : alphaInt B = pInt B } ; :: deftheorem defines D(alpha,s) DECOMP_1:def_21_:_ for T being TopSpace holds D(alpha,s) T = { B where B is Subset of T : alphaInt B = sInt B } ; :: deftheorem defines D(alpha,ps) DECOMP_1:def_22_:_ for T being TopSpace holds D(alpha,ps) T = { B where B is Subset of T : alphaInt B = psInt B } ; :: deftheorem defines D(p,sp) DECOMP_1:def_23_:_ for T being TopSpace holds D(p,sp) T = { B where B is Subset of T : pInt B = spInt B } ; :: deftheorem defines D(p,ps) DECOMP_1:def_24_:_ for T being TopSpace holds D(p,ps) T = { B where B is Subset of T : pInt B = psInt B } ; :: deftheorem defines D(sp,ps) DECOMP_1:def_25_:_ for T being TopSpace holds D(sp,ps) T = { B where B is Subset of T : spInt B = psInt B } ; theorem Th1: :: DECOMP_1:1 for T being TopSpace for B being Subset of T holds ( alphaInt B = pInt B iff sInt B = psInt B ) proof let T be TopSpace; ::_thesis: for B being Subset of T holds ( alphaInt B = pInt B iff sInt B = psInt B ) let B be Subset of T; ::_thesis: ( alphaInt B = pInt B iff sInt B = psInt B ) hereby ::_thesis: ( sInt B = psInt B implies alphaInt B = pInt B ) 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 ; ::_thesis: sInt B = psInt 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, XBOOLE_0:def_10; ::_thesis: verum end; A3: Int (Cl B) c= Cl (Int (Cl B)) by PRE_TOPC:18; assume psInt B = sInt B ; ::_thesis: alphaInt B = pInt 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, XBOOLE_1:1; 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, XBOOLE_1:1; 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 alphaInt B = pInt B by A6, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th2: :: DECOMP_1:2 for T being TopSpace for B being Subset of T holds ( B is alpha-set of T iff B = alphaInt B ) proof let T be TopSpace; ::_thesis: for B being Subset of T holds ( B is alpha-set of T iff B = alphaInt B ) let B be Subset of T; ::_thesis: ( B is alpha-set of T iff B = alphaInt B ) hereby ::_thesis: ( B = alphaInt B implies B is alpha-set of T ) assume B is alpha-set of T ; ::_thesis: B = alphaInt B then B c= Int (Cl (Int B)) by Def1; hence B = alphaInt B by XBOOLE_1:28; ::_thesis: verum end; assume B = alphaInt B ; ::_thesis: B is alpha-set of T then B c= Int (Cl (Int B)) by XBOOLE_1:17; hence B is alpha-set of T by Def1; ::_thesis: verum end; theorem Th3: :: DECOMP_1:3 for T being TopSpace for B being Subset of T holds ( B is semi-open iff B = sInt B ) proof let T be TopSpace; ::_thesis: for B being Subset of T holds ( B is semi-open iff B = sInt B ) let B be Subset of T; ::_thesis: ( B is semi-open iff B = sInt B ) hereby ::_thesis: ( B = sInt B implies B is semi-open ) assume B is semi-open ; ::_thesis: B = sInt B then B c= Cl (Int B) by Def2; hence B = sInt B by XBOOLE_1:28; ::_thesis: verum end; assume B = sInt B ; ::_thesis: B is semi-open then B c= Cl (Int B) by XBOOLE_1:17; hence B is semi-open by Def2; ::_thesis: verum end; theorem Th4: :: DECOMP_1:4 for T being TopSpace for B being Subset of T holds ( B is pre-open iff B = pInt B ) proof let T be TopSpace; ::_thesis: for B being Subset of T holds ( B is pre-open iff B = pInt B ) let B be Subset of T; ::_thesis: ( B is pre-open iff B = pInt B ) hereby ::_thesis: ( B = pInt B implies B is pre-open ) assume B is pre-open ; ::_thesis: B = pInt B then B c= Int (Cl B) by Def3; hence B = pInt B by XBOOLE_1:28; ::_thesis: verum end; assume B = pInt B ; ::_thesis: B is pre-open then B c= Int (Cl B) by XBOOLE_1:17; hence B is pre-open by Def3; ::_thesis: verum end; theorem Th5: :: DECOMP_1:5 for T being TopSpace for B being Subset of T holds ( B is pre-semi-open iff B = psInt B ) proof let T be TopSpace; ::_thesis: for B being Subset of T holds ( B is pre-semi-open iff B = psInt B ) let B be Subset of T; ::_thesis: ( B is pre-semi-open iff B = psInt B ) hereby ::_thesis: ( B = psInt B implies B is pre-semi-open ) assume B is pre-semi-open ; ::_thesis: B = psInt B then B c= Cl (Int (Cl B)) by Def4; hence B = psInt B by XBOOLE_1:28; ::_thesis: verum end; assume B = psInt B ; ::_thesis: B is pre-semi-open then B c= Cl (Int (Cl B)) by XBOOLE_1:17; hence B is pre-semi-open by Def4; ::_thesis: verum end; theorem Th6: :: DECOMP_1:6 for T being TopSpace for B being Subset of T holds ( B is semi-pre-open iff B = spInt B ) proof let T be TopSpace; ::_thesis: for B being Subset of T holds ( B is semi-pre-open iff B = spInt B ) let B be Subset of T; ::_thesis: ( B is semi-pre-open iff B = spInt B ) hereby ::_thesis: ( B = spInt B implies B is semi-pre-open ) assume B is semi-pre-open ; ::_thesis: B = spInt B then B c= (Cl (Int B)) \/ (Int (Cl B)) by Def5; then B = B /\ ((Cl (Int B)) \/ (Int (Cl B))) by XBOOLE_1:28; hence B = spInt B by XBOOLE_1:23; ::_thesis: verum end; assume B = spInt B ; ::_thesis: B is semi-pre-open then B = B /\ ((Cl (Int B)) \/ (Int (Cl B))) by XBOOLE_1:23; then B c= (Cl (Int B)) \/ (Int (Cl B)) by XBOOLE_1:17; hence B is semi-pre-open by Def5; ::_thesis: verum end; theorem Th7: :: DECOMP_1:7 for T being TopSpace holds (T ^alpha) /\ (D(c,alpha) T) = the topology of T proof let T be TopSpace; ::_thesis: (T ^alpha) /\ (D(c,alpha) T) = the topology of T thus (T ^alpha) /\ (D(c,alpha) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (T ^alpha) /\ (D(c,alpha) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (T ^alpha) /\ (D(c,alpha) T) or x in the topology of T ) assume A1: x in (T ^alpha) /\ (D(c,alpha) T) ; ::_thesis: x in the topology of T then x in T ^alpha by XBOOLE_0:def_4; then consider A being 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 being 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 x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (T ^alpha) /\ (D(c,alpha) T) ) assume A6: x in the topology of T ; ::_thesis: x in (T ^alpha) /\ (D(c,alpha) 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 where B is Subset of T : Int B = alphaInt B } ; K in T ^alpha by A8; hence x in (T ^alpha) /\ (D(c,alpha) T) by A9, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th8: :: DECOMP_1:8 for T being TopSpace holds (SO T) /\ (D(c,s) T) = the topology of T proof let T be TopSpace; ::_thesis: (SO T) /\ (D(c,s) T) = the topology of T thus (SO T) /\ (D(c,s) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (SO T) /\ (D(c,s) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (SO T) /\ (D(c,s) T) or x in the topology of T ) assume A1: x in (SO T) /\ (D(c,s) T) ; ::_thesis: x in the topology of T then x in SO T by XBOOLE_0:def_4; then consider A being 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 being Subset of T such that A4: x = Z and A5: Int Z = sInt Z ; A = sInt A by A3, Th3; then Z is open by A2, A4, A5; hence x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (SO T) /\ (D(c,s) T) ) assume A6: x in the topology of T ; ::_thesis: x in (SO T) /\ (D(c,s) 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= Cl (Int K) by PRE_TOPC:18; then A8: K is semi-open by Def2; then Int K = sInt K by A7, Th3; then A9: K in { B where B is Subset of T : Int B = sInt B } ; K in SO T by A8; hence x in (SO T) /\ (D(c,s) T) by A9, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th9: :: DECOMP_1:9 for T being TopSpace holds (PO T) /\ (D(c,p) T) = the topology of T proof let T be TopSpace; ::_thesis: (PO T) /\ (D(c,p) T) = the topology of T thus (PO T) /\ (D(c,p) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (PO T) /\ (D(c,p) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PO T) /\ (D(c,p) T) or x in the topology of T ) assume A1: x in (PO T) /\ (D(c,p) T) ; ::_thesis: x in the topology of T then x in PO T by XBOOLE_0:def_4; then consider A being 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 being Subset of T such that A4: x = Z and A5: Int Z = pInt Z ; A = pInt A by A3, Th4; then Z is open by A2, A4, A5; hence x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (PO T) /\ (D(c,p) T) ) assume A6: x in the topology of T ; ::_thesis: x in (PO T) /\ (D(c,p) 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 K) by PRE_TOPC:18, TOPS_1:19; then A8: K is pre-open by Def3; then Int K = pInt K by A7, Th4; then A9: K in { B where B is Subset of T : Int B = pInt B } ; K in PO T by A8; hence x in (PO T) /\ (D(c,p) T) by A9, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th10: :: DECOMP_1:10 for T being TopSpace holds (PSO T) /\ (D(c,ps) T) = the topology of T proof let T be TopSpace; ::_thesis: (PSO T) /\ (D(c,ps) T) = the topology of T thus (PSO T) /\ (D(c,ps) T) c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= (PSO T) /\ (D(c,ps) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(c,ps) T) or x in the topology of T ) assume A1: x in (PSO T) /\ (D(c,ps) T) ; ::_thesis: x in the topology of T then x in PSO T by XBOOLE_0:def_4; then consider A being 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 being Subset of T such that A4: x = Z and A5: Int Z = psInt Z ; A = psInt A by A3, Th5; then Z is open by A2, A4, A5; hence x in the topology of T by A4, PRE_TOPC:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T or x in (PSO T) /\ (D(c,ps) T) ) assume A6: x in the topology of T ; ::_thesis: x in (PSO T) /\ (D(c,ps) 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, XBOOLE_1:1; then A9: K is pre-semi-open by Def4; then Int K = psInt K by A8, Th5; then A10: K in { B where B is Subset of T : Int B = psInt B } ; K in PSO T by A9; hence x in (PSO T) /\ (D(c,ps) T) by A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th11: :: DECOMP_1:11 for T being TopSpace holds (PO T) /\ (D(alpha,p) T) = T ^alpha proof let T be TopSpace; ::_thesis: (PO T) /\ (D(alpha,p) T) = T ^alpha thus (PO T) /\ (D(alpha,p) T) c= T ^alpha :: according to XBOOLE_0:def_10 ::_thesis: T ^alpha c= (PO T) /\ (D(alpha,p) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PO T) /\ (D(alpha,p) T) or x in T ^alpha ) assume A1: x in (PO T) /\ (D(alpha,p) T) ; ::_thesis: x in T ^alpha then x in PO T by XBOOLE_0:def_4; then consider A being 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 being 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 x in T ^alpha by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T ^alpha or x in (PO T) /\ (D(alpha,p) T) ) assume x in T ^alpha ; ::_thesis: x in (PO T) /\ (D(alpha,p) T) then consider K being 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, XBOOLE_1:1; then A9: K is pre-open by Def3; then K = pInt K by Th4; then alphaInt K = pInt K by A7, Th2; then A10: K in { B where B is Subset of T : alphaInt B = pInt B } ; K in PO T by A9; hence x in (PO T) /\ (D(alpha,p) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th12: :: DECOMP_1:12 for T being TopSpace holds (SO T) /\ (D(alpha,s) T) = T ^alpha proof let T be TopSpace; ::_thesis: (SO T) /\ (D(alpha,s) T) = T ^alpha thus (SO T) /\ (D(alpha,s) T) c= T ^alpha :: according to XBOOLE_0:def_10 ::_thesis: T ^alpha c= (SO T) /\ (D(alpha,s) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (SO T) /\ (D(alpha,s) T) or x in T ^alpha ) assume A1: x in (SO T) /\ (D(alpha,s) T) ; ::_thesis: x in T ^alpha then x in SO T by XBOOLE_0:def_4; then consider A being 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 being Subset of T such that A4: x = Z and A5: alphaInt Z = sInt Z ; A = sInt A by A3, Th3; then Z is alpha-set of T by A2, A4, A5, Th2; hence x in T ^alpha by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T ^alpha or x in (SO T) /\ (D(alpha,s) T) ) assume x in T ^alpha ; ::_thesis: x in (SO T) /\ (D(alpha,s) T) then consider K being 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, XBOOLE_1:1; then A9: K is semi-open by Def2; then K = sInt K by Th3; then alphaInt K = sInt K by A7, Th2; then A10: K in { B where B is Subset of T : alphaInt B = sInt B } ; K in { B where B is Subset of T : B is semi-open } by A9; hence x in (SO T) /\ (D(alpha,s) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th13: :: DECOMP_1:13 for T being TopSpace holds (PSO T) /\ (D(alpha,ps) T) = T ^alpha proof let T be TopSpace; ::_thesis: (PSO T) /\ (D(alpha,ps) T) = T ^alpha thus (PSO T) /\ (D(alpha,ps) T) c= T ^alpha :: according to XBOOLE_0:def_10 ::_thesis: T ^alpha c= (PSO T) /\ (D(alpha,ps) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(alpha,ps) T) or x in T ^alpha ) assume A1: x in (PSO T) /\ (D(alpha,ps) T) ; ::_thesis: x in T ^alpha then x in PSO T by XBOOLE_0:def_4; then consider A being 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 being 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 x in T ^alpha by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T ^alpha or x in (PSO T) /\ (D(alpha,ps) T) ) assume x in T ^alpha ; ::_thesis: x in (PSO T) /\ (D(alpha,ps) T) then consider K being 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, XBOOLE_1:1; K c= Int (Cl (Int K)) by A7, Def1; then K c= Cl (Int (Cl K)) by A9, XBOOLE_1:1; then A10: K is pre-semi-open by Def4; then K = psInt K by Th5; then alphaInt K = psInt K by A7, Th2; then A11: K in { B where B is Subset of T : alphaInt B = psInt B } ; K in PSO T by A10; hence x in (PSO T) /\ (D(alpha,ps) T) by A6, A11, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th14: :: DECOMP_1:14 for T being TopSpace holds (SPO T) /\ (D(p,sp) T) = PO T proof let T be TopSpace; ::_thesis: (SPO T) /\ (D(p,sp) T) = PO T thus (SPO T) /\ (D(p,sp) T) c= PO T :: according to XBOOLE_0:def_10 ::_thesis: PO T c= (SPO T) /\ (D(p,sp) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (SPO T) /\ (D(p,sp) T) or x in PO T ) assume A1: x in (SPO T) /\ (D(p,sp) T) ; ::_thesis: x in PO T then x in SPO T by XBOOLE_0:def_4; then consider A being Subset of T such that A2: x = A and A3: A is semi-pre-open ; x in D(p,sp) T by A1, XBOOLE_0:def_4; then consider Z being Subset of T such that A4: x = Z and A5: pInt Z = spInt Z ; A = spInt A by A3, Th6; then Z is pre-open by A2, A4, A5, Th4; hence x in PO T by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PO T or x in (SPO T) /\ (D(p,sp) T) ) assume x in PO T ; ::_thesis: x in (SPO T) /\ (D(p,sp) T) then consider K being Subset of T such that A6: x = K and A7: K is pre-open ; A8: Int (Cl K) c= (Cl (Int K)) \/ (Int (Cl K)) by XBOOLE_1:7; K c= Int (Cl K) by A7, Def3; then K c= (Cl (Int K)) \/ (Int (Cl K)) by A8, XBOOLE_1:1; then A9: K is semi-pre-open by Def5; then K = spInt K by Th6; then pInt K = spInt K by A7, Th4; then A10: K in { B where B is Subset of T : pInt B = spInt B } ; K in SPO T by A9; hence x in (SPO T) /\ (D(p,sp) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th15: :: DECOMP_1:15 for T being TopSpace holds (PSO T) /\ (D(p,ps) T) = PO T proof let T be TopSpace; ::_thesis: (PSO T) /\ (D(p,ps) T) = PO T thus (PSO T) /\ (D(p,ps) T) c= PO T :: according to XBOOLE_0:def_10 ::_thesis: PO T c= (PSO T) /\ (D(p,ps) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(p,ps) T) or x in PO T ) assume A1: x in (PSO T) /\ (D(p,ps) T) ; ::_thesis: x in PO T then x in PSO T by XBOOLE_0:def_4; then consider A being Subset of T such that A2: x = A and A3: A is pre-semi-open ; x in D(p,ps) T by A1, XBOOLE_0:def_4; then consider Z being Subset of T such that A4: x = Z and A5: pInt Z = psInt Z ; A = psInt A by A3, Th5; then Z is pre-open by A2, A4, A5, Th4; hence x in PO T by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PO T or x in (PSO T) /\ (D(p,ps) T) ) assume x in PO T ; ::_thesis: x in (PSO T) /\ (D(p,ps) T) then consider K being Subset of T such that A6: x = K and A7: K is pre-open ; A8: Int (Cl K) c= Cl (Int (Cl K)) by PRE_TOPC:18; K c= Int (Cl K) by A7, Def3; then K c= Cl (Int (Cl K)) by A8, XBOOLE_1:1; then A9: K is pre-semi-open by Def4; then K = psInt K by Th5; then pInt K = psInt K by A7, Th4; then A10: K in { B where B is Subset of T : pInt B = psInt B } ; K in PSO T by A9; hence x in (PSO T) /\ (D(p,ps) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th16: :: DECOMP_1:16 for T being TopSpace holds (PSO T) /\ (D(alpha,p) T) = SO T proof let T be TopSpace; ::_thesis: (PSO T) /\ (D(alpha,p) T) = SO T thus (PSO T) /\ (D(alpha,p) T) c= SO T :: according to XBOOLE_0:def_10 ::_thesis: SO T c= (PSO T) /\ (D(alpha,p) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(alpha,p) T) or x in SO T ) assume A1: x in (PSO T) /\ (D(alpha,p) T) ; ::_thesis: x in SO T then x in PSO T by XBOOLE_0:def_4; then consider A being Subset of T such that A2: x = A and A3: A is pre-semi-open ; x in D(alpha,p) T by A1, XBOOLE_0:def_4; then consider Z being Subset of T such that A4: x = Z and A5: alphaInt Z = pInt Z ; A = psInt A by A3, Th5; then Z = sInt Z by A2, A4, A5, Th1; then Z is semi-open by Th3; hence x in SO T by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SO T or x in (PSO T) /\ (D(alpha,p) T) ) assume x in SO T ; ::_thesis: x in (PSO T) /\ (D(alpha,p) T) then consider K being Subset of T such that A6: x = K and A7: 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 A8: Cl (Int K) c= Cl (Int (Cl K)) by TOPS_1:26; K c= Cl (Int K) by A7, Def2; then K c= Cl (Int (Cl K)) by A8, XBOOLE_1:1; then A9: K is pre-semi-open by Def4; then K = psInt K by Th5; then sInt K = psInt K by A7, Th3; then alphaInt K = pInt K by Th1; then A10: K in { B where B is Subset of T : alphaInt B = pInt B } ; K in PSO T by A9; hence x in (PSO T) /\ (D(alpha,p) T) by A6, A10, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th17: :: DECOMP_1:17 for T being TopSpace holds (PSO T) /\ (D(sp,ps) T) = SPO T proof let T be TopSpace; ::_thesis: (PSO T) /\ (D(sp,ps) T) = SPO T thus (PSO T) /\ (D(sp,ps) T) c= SPO T :: according to XBOOLE_0:def_10 ::_thesis: SPO T c= (PSO T) /\ (D(sp,ps) T) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (PSO T) /\ (D(sp,ps) T) or x in SPO T ) assume A1: x in (PSO T) /\ (D(sp,ps) T) ; ::_thesis: x in SPO T then x in PSO T by XBOOLE_0:def_4; then consider A being Subset of T such that A2: x = A and A3: A is pre-semi-open ; x in D(sp,ps) T by A1, XBOOLE_0:def_4; then consider Z being Subset of T such that A4: x = Z and A5: spInt Z = psInt Z ; A = psInt A by A3, Th5; then Z is semi-pre-open by A2, A4, A5, Th6; hence x in SPO T by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SPO T or x in (PSO T) /\ (D(sp,ps) T) ) assume x in SPO T ; ::_thesis: x in (PSO T) /\ (D(sp,ps) T) then consider K being Subset of T such that A6: x = K and A7: 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 A8: 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 A9: (Cl (Int K)) \/ (Int (Cl K)) c= Cl (Int (Cl K)) by A8, XBOOLE_1:8; K c= (Cl (Int K)) \/ (Int (Cl K)) by A7, Def5; then K c= Cl (Int (Cl K)) by A9, XBOOLE_1:1; then A10: K is pre-semi-open by Def4; then K = psInt K by Th5; then spInt K = psInt K by A7, Th6; then A11: K in { B where B is Subset of T : spInt B = psInt B } ; K in PSO T by A10; hence x in (PSO T) /\ (D(sp,ps) T) by A6, A11, XBOOLE_0:def_4; ::_thesis: verum end; definition let X, Y be non empty TopSpace; let f be Function of X,Y; attrf is s-continuous means :Def26: :: DECOMP_1:def 26 for G being Subset of Y st G is open holds f " G in SO X; attrf is p-continuous means :Def27: :: DECOMP_1:def 27 for G being Subset of Y st G is open holds f " G in PO X; attrf is alpha-continuous means :Def28: :: DECOMP_1:def 28 for G being Subset of Y st G is open holds f " G in X ^alpha ; attrf is ps-continuous means :Def29: :: DECOMP_1:def 29 for G being Subset of Y st G is open holds f " G in PSO X; attrf is sp-continuous means :Def30: :: DECOMP_1:def 30 for G being Subset of Y st G is open holds f " G in SPO X; attrf is (c,alpha)-continuous means :Def31: :: DECOMP_1:def 31 for G being Subset of Y st G is open holds f " G in D(c,alpha) X; attrf is (c,s)-continuous means :Def32: :: DECOMP_1:def 32 for G being Subset of Y st G is open holds f " G in D(c,s) X; attrf is (c,p)-continuous means :Def33: :: DECOMP_1:def 33 for G being Subset of Y st G is open holds f " G in D(c,p) X; attrf is (c,ps)-continuous means :Def34: :: DECOMP_1:def 34 for G being Subset of Y st G is open holds f " G in D(c,ps) X; attrf is (alpha,p)-continuous means :Def35: :: DECOMP_1:def 35 for G being Subset of Y st G is open holds f " G in D(alpha,p) X; attrf is (alpha,s)-continuous means :Def36: :: DECOMP_1:def 36 for G being Subset of Y st G is open holds f " G in D(alpha,s) X; attrf is (alpha,ps)-continuous means :Def37: :: DECOMP_1:def 37 for G being Subset of Y st G is open holds f " G in D(alpha,ps) X; attrf is (p,ps)-continuous means :: DECOMP_1:def 38 for G being Subset of Y st G is open holds f " G in D(p,ps) X; attrf is (p,sp)-continuous means :: DECOMP_1:def 39 for G being Subset of Y st G is open holds f " G in D(p,sp) X; attrf is (sp,ps)-continuous means :: DECOMP_1:def 40 for G being Subset of Y st G is open holds f " G in D(sp,ps) X; end; :: deftheorem Def26 defines s-continuous DECOMP_1:def_26_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is s-continuous iff for G being Subset of Y st G is open holds f " G in SO X ); :: deftheorem Def27 defines p-continuous DECOMP_1:def_27_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is p-continuous iff for G being Subset of Y st G is open holds f " G in PO X ); :: deftheorem Def28 defines alpha-continuous DECOMP_1:def_28_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is alpha-continuous iff for G being Subset of Y st G is open holds f " G in X ^alpha ); :: deftheorem Def29 defines ps-continuous DECOMP_1:def_29_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is ps-continuous iff for G being Subset of Y st G is open holds f " G in PSO X ); :: deftheorem Def30 defines sp-continuous DECOMP_1:def_30_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is sp-continuous iff for G being Subset of Y st G is open holds f " G in SPO X ); :: deftheorem Def31 defines (c,alpha)-continuous DECOMP_1:def_31_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (c,alpha)-continuous iff for G being Subset of Y st G is open holds f " G in D(c,alpha) X ); :: deftheorem Def32 defines (c,s)-continuous DECOMP_1:def_32_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (c,s)-continuous iff for G being Subset of Y st G is open holds f " G in D(c,s) X ); :: deftheorem Def33 defines (c,p)-continuous DECOMP_1:def_33_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (c,p)-continuous iff for G being Subset of Y st G is open holds f " G in D(c,p) X ); :: deftheorem Def34 defines (c,ps)-continuous DECOMP_1:def_34_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (c,ps)-continuous iff for G being Subset of Y st G is open holds f " G in D(c,ps) X ); :: deftheorem Def35 defines (alpha,p)-continuous DECOMP_1:def_35_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (alpha,p)-continuous iff for G being Subset of Y st G is open holds f " G in D(alpha,p) X ); :: deftheorem Def36 defines (alpha,s)-continuous DECOMP_1:def_36_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (alpha,s)-continuous iff for G being Subset of Y st G is open holds f " G in D(alpha,s) X ); :: deftheorem Def37 defines (alpha,ps)-continuous DECOMP_1:def_37_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (alpha,ps)-continuous iff for G being Subset of Y st G is open holds f " G in D(alpha,ps) X ); :: deftheorem defines (p,ps)-continuous DECOMP_1:def_38_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (p,ps)-continuous iff for G being Subset of Y st G is open holds f " G in D(p,ps) X ); :: deftheorem defines (p,sp)-continuous DECOMP_1:def_39_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (p,sp)-continuous iff for G being Subset of Y st G is open holds f " G in D(p,sp) X ); :: deftheorem defines (sp,ps)-continuous DECOMP_1:def_40_:_ for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is (sp,ps)-continuous iff for G being Subset of Y st G is open holds f " G in D(sp,ps) X ); theorem :: DECOMP_1:18 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is alpha-continuous iff ( f is p-continuous & f is (alpha,p)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is alpha-continuous iff ( f is p-continuous & f is (alpha,p)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is alpha-continuous iff ( f is p-continuous & f is (alpha,p)-continuous ) ) hereby ::_thesis: ( f is p-continuous & f is (alpha,p)-continuous implies f is alpha-continuous ) assume A1: f is alpha-continuous ; ::_thesis: ( f is p-continuous & f is (alpha,p)-continuous ) thus f is p-continuous ::_thesis: f is (alpha,p)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X ) assume V is open ; ::_thesis: f " V in PO X then f " V in X ^alpha by A1, Def28; then f " V in (PO X) /\ (D(alpha,p) X) by Th11; hence f " V in PO X by XBOOLE_0:def_4; ::_thesis: verum end; thus f is (alpha,p)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_35 ::_thesis: ( G is open implies f " G in D(alpha,p) X ) assume G is open ; ::_thesis: f " G in D(alpha,p) X then f " G in X ^alpha by A1, Def28; then f " G in (PO X) /\ (D(alpha,p) X) by Th11; hence f " G in D(alpha,p) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A2: ( f is p-continuous & f is (alpha,p)-continuous ) ; ::_thesis: f is alpha-continuous let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha ) assume V is open ; ::_thesis: f " V in X ^alpha then ( f " V in PO X & f " V in D(alpha,p) X ) by A2, Def27, Def35; then f " V in (PO X) /\ (D(alpha,p) X) by XBOOLE_0:def_4; hence f " V in X ^alpha by Th11; ::_thesis: verum end; theorem :: DECOMP_1:19 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is alpha-continuous iff ( f is s-continuous & f is (alpha,s)-continuous ) ) hereby ::_thesis: ( f is s-continuous & f is (alpha,s)-continuous implies f is alpha-continuous ) assume A1: f is alpha-continuous ; ::_thesis: ( f is s-continuous & f is (alpha,s)-continuous ) thus f is s-continuous ::_thesis: f is (alpha,s)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_26 ::_thesis: ( V is open implies f " V in SO X ) assume V is open ; ::_thesis: f " V in SO X then f " V in X ^alpha by A1, Def28; then f " V in (SO X) /\ (D(alpha,s) X) by Th12; hence f " V in SO X by XBOOLE_0:def_4; ::_thesis: verum end; thus f is (alpha,s)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_36 ::_thesis: ( G is open implies f " G in D(alpha,s) X ) assume G is open ; ::_thesis: f " G in D(alpha,s) X then f " G in X ^alpha by A1, Def28; then f " G in (SO X) /\ (D(alpha,s) X) by Th12; hence f " G in D(alpha,s) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A2: ( f is s-continuous & f is (alpha,s)-continuous ) ; ::_thesis: f is alpha-continuous let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha ) assume V is open ; ::_thesis: f " V in X ^alpha then ( f " V in SO X & f " V in D(alpha,s) X ) by A2, Def26, Def36; then f " V in (SO X) /\ (D(alpha,s) X) by XBOOLE_0:def_4; hence f " V in X ^alpha by Th12; ::_thesis: verum end; theorem :: DECOMP_1:20 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is alpha-continuous iff ( f is ps-continuous & f is (alpha,ps)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is alpha-continuous iff ( f is ps-continuous & f is (alpha,ps)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is alpha-continuous iff ( f is ps-continuous & f is (alpha,ps)-continuous ) ) hereby ::_thesis: ( f is ps-continuous & f is (alpha,ps)-continuous implies f is alpha-continuous ) assume A1: f is alpha-continuous ; ::_thesis: ( f is ps-continuous & f is (alpha,ps)-continuous ) thus f is ps-continuous ::_thesis: f is (alpha,ps)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X ) assume V is open ; ::_thesis: f " V in PSO X then f " V in X ^alpha by A1, Def28; then f " V in (PSO X) /\ (D(alpha,ps) X) by Th13; hence f " V in PSO X by XBOOLE_0:def_4; ::_thesis: verum end; thus f is (alpha,ps)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_37 ::_thesis: ( G is open implies f " G in D(alpha,ps) X ) assume G is open ; ::_thesis: f " G in D(alpha,ps) X then f " G in X ^alpha by A1, Def28; then f " G in (PSO X) /\ (D(alpha,ps) X) by Th13; hence f " G in D(alpha,ps) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A2: ( f is ps-continuous & f is (alpha,ps)-continuous ) ; ::_thesis: f is alpha-continuous let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha ) assume V is open ; ::_thesis: f " V in X ^alpha then ( f " V in PSO X & f " V in D(alpha,ps) X ) by A2, Def29, Def37; then f " V in (PSO X) /\ (D(alpha,ps) X) by XBOOLE_0:def_4; hence f " V in X ^alpha by Th13; ::_thesis: verum end; theorem :: DECOMP_1:21 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is p-continuous iff ( f is sp-continuous & f is (p,sp)-continuous ) ) hereby ::_thesis: ( f is sp-continuous & f is (p,sp)-continuous implies f is p-continuous ) assume A1: f is p-continuous ; ::_thesis: ( f is sp-continuous & f is (p,sp)-continuous ) thus f is sp-continuous ::_thesis: f is (p,sp)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_30 ::_thesis: ( V is open implies f " V in SPO X ) assume V is open ; ::_thesis: f " V in SPO X then f " V in PO X by A1, Def27; hence f " V in SPO X ; ::_thesis: verum end; thus f is (p,sp)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_39 ::_thesis: ( G is open implies f " G in D(p,sp) X ) assume G is open ; ::_thesis: f " G in D(p,sp) X then f " G in PO X by A1, Def27; then f " G in (SPO X) /\ (D(p,sp) X) by Th14; hence f " G in D(p,sp) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A2: ( f is sp-continuous & f is (p,sp)-continuous ) ; ::_thesis: f is p-continuous let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X ) assume V is open ; ::_thesis: f " V in PO X then f " V in SPO X by A2, Def30; hence f " V in PO X ; ::_thesis: verum end; theorem :: DECOMP_1:22 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is p-continuous iff ( f is ps-continuous & f is (p,ps)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is p-continuous iff ( f is ps-continuous & f is (p,ps)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is p-continuous iff ( f is ps-continuous & f is (p,ps)-continuous ) ) hereby ::_thesis: ( f is ps-continuous & f is (p,ps)-continuous implies f is p-continuous ) assume A1: f is p-continuous ; ::_thesis: ( f is ps-continuous & f is (p,ps)-continuous ) thus f is ps-continuous ::_thesis: f is (p,ps)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X ) assume V is open ; ::_thesis: f " V in PSO X then f " V in PO X by A1, Def27; hence f " V in PSO X ; ::_thesis: verum end; thus f is (p,ps)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_38 ::_thesis: ( G is open implies f " G in D(p,ps) X ) assume G is open ; ::_thesis: f " G in D(p,ps) X then f " G in PO X by A1, Def27; then f " G in (PSO X) /\ (D(p,ps) X) by Th15; hence f " G in D(p,ps) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A2: ( f is ps-continuous & f is (p,ps)-continuous ) ; ::_thesis: f is p-continuous let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X ) assume V is open ; ::_thesis: f " V in PO X then f " V in PSO X by A2, Def29; hence f " V in PO X ; ::_thesis: verum end; theorem :: DECOMP_1:23 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is s-continuous iff ( f is ps-continuous & f is (alpha,p)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is s-continuous iff ( f is ps-continuous & f is (alpha,p)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is s-continuous iff ( f is ps-continuous & f is (alpha,p)-continuous ) ) hereby ::_thesis: ( f is ps-continuous & f is (alpha,p)-continuous implies f is s-continuous ) assume A1: f is s-continuous ; ::_thesis: ( f is ps-continuous & f is (alpha,p)-continuous ) thus f is ps-continuous ::_thesis: f is (alpha,p)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X ) assume V is open ; ::_thesis: f " V in PSO X then f " V in SO X by A1, Def26; hence f " V in PSO X ; ::_thesis: verum end; thus f is (alpha,p)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_35 ::_thesis: ( G is open implies f " G in D(alpha,p) X ) assume G is open ; ::_thesis: f " G in D(alpha,p) X then f " G in SO X by A1, Def26; then f " G in (PSO X) /\ (D(alpha,p) X) by Th16; hence f " G in D(alpha,p) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A2: ( f is ps-continuous & f is (alpha,p)-continuous ) ; ::_thesis: f is s-continuous let V be Subset of Y; :: according to DECOMP_1:def_26 ::_thesis: ( V is open implies f " V in SO X ) assume V is open ; ::_thesis: f " V in SO X then f " V in PSO X by A2, Def29; hence f " V in SO X ; ::_thesis: verum end; theorem :: DECOMP_1:24 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is sp-continuous iff ( f is ps-continuous & f is (sp,ps)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is sp-continuous iff ( f is ps-continuous & f is (sp,ps)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is sp-continuous iff ( f is ps-continuous & f is (sp,ps)-continuous ) ) hereby ::_thesis: ( f is ps-continuous & f is (sp,ps)-continuous implies f is sp-continuous ) assume A1: f is sp-continuous ; ::_thesis: ( f is ps-continuous & f is (sp,ps)-continuous ) thus f is ps-continuous ::_thesis: f is (sp,ps)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X ) assume V is open ; ::_thesis: f " V in PSO X then f " V in SPO X by A1, Def30; hence f " V in PSO X ; ::_thesis: verum end; thus f is (sp,ps)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_40 ::_thesis: ( G is open implies f " G in D(sp,ps) X ) assume G is open ; ::_thesis: f " G in D(sp,ps) X then f " G in SPO X by A1, Def30; then f " G in (PSO X) /\ (D(sp,ps) X) by Th17; hence f " G in D(sp,ps) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A2: ( f is ps-continuous & f is (sp,ps)-continuous ) ; ::_thesis: f is sp-continuous let V be Subset of Y; :: according to DECOMP_1:def_30 ::_thesis: ( V is open implies f " V in SPO X ) assume V is open ; ::_thesis: f " V in SPO X then f " V in PSO X by A2, Def29; hence f " V in SPO X ; ::_thesis: verum end; theorem :: DECOMP_1:25 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is continuous iff ( f is alpha-continuous & f is (c,alpha)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is continuous iff ( f is alpha-continuous & f is (c,alpha)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is alpha-continuous & f is (c,alpha)-continuous ) ) A1: [#] Y <> {} ; hereby ::_thesis: ( f is alpha-continuous & f is (c,alpha)-continuous implies f is continuous ) assume A2: f is continuous ; ::_thesis: ( f is alpha-continuous & f is (c,alpha)-continuous ) thus f is alpha-continuous ::_thesis: f is (c,alpha)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_28 ::_thesis: ( V is open implies f " V in X ^alpha ) assume V is open ; ::_thesis: f " V in X ^alpha 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 f " V in X ^alpha by XBOOLE_0:def_4; ::_thesis: verum end; thus f is (c,alpha)-continuous ::_thesis: verum proof let G be Subset of Y; :: according to DECOMP_1:def_31 ::_thesis: ( G is open implies f " G in D(c,alpha) X ) assume G is open ; ::_thesis: f " G in D(c,alpha) X 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 f " G in D(c,alpha) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A3: ( f is alpha-continuous & f is (c,alpha)-continuous ) ; ::_thesis: f is continuous now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_ f_"_V_is_open let V be Subset of Y; ::_thesis: ( V is open implies f " V is open ) assume V is open ; ::_thesis: f " V is open then ( f " V in X ^alpha & f " V in D(c,alpha) X ) by A3, Def28, Def31; 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; ::_thesis: verum end; hence f is continuous by A1, TOPS_2:43; ::_thesis: verum end; theorem :: DECOMP_1:26 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is continuous iff ( f is s-continuous & f is (c,s)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is continuous iff ( f is s-continuous & f is (c,s)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is s-continuous & f is (c,s)-continuous ) ) A1: [#] Y <> {} ; hereby ::_thesis: ( f is s-continuous & f is (c,s)-continuous implies f is continuous ) assume A2: f is continuous ; ::_thesis: ( f is s-continuous & f is (c,s)-continuous ) thus f is s-continuous ::_thesis: f is (c,s)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_26 ::_thesis: ( V is open implies f " V in SO X ) assume V is open ; ::_thesis: f " V in SO X 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 f " V in SO X by XBOOLE_0:def_4; ::_thesis: verum end; thus f is (c,s)-continuous ::_thesis: verum proof let V be Subset of Y; :: according to DECOMP_1:def_32 ::_thesis: ( V is open implies f " V in D(c,s) X ) assume V is open ; ::_thesis: f " V in D(c,s) X 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 f " V in D(c,s) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A3: ( f is s-continuous & f is (c,s)-continuous ) ; ::_thesis: f is continuous now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_ f_"_V_is_open let V be Subset of Y; ::_thesis: ( V is open implies f " V is open ) assume V is open ; ::_thesis: f " V is open then ( f " V in SO X & f " V in D(c,s) X ) by A3, Def26, Def32; 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; ::_thesis: verum end; hence f is continuous by A1, TOPS_2:43; ::_thesis: verum end; theorem :: DECOMP_1:27 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is p-continuous & f is (c,p)-continuous ) ) A1: [#] Y <> {} ; hereby ::_thesis: ( f is p-continuous & f is (c,p)-continuous implies f is continuous ) assume A2: f is continuous ; ::_thesis: ( f is p-continuous & f is (c,p)-continuous ) thus f is p-continuous ::_thesis: f is (c,p)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_27 ::_thesis: ( V is open implies f " V in PO X ) assume V is open ; ::_thesis: f " V in PO X 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 f " V in PO X by XBOOLE_0:def_4; ::_thesis: verum end; thus f is (c,p)-continuous ::_thesis: verum proof let V be Subset of Y; :: according to DECOMP_1:def_33 ::_thesis: ( V is open implies f " V in D(c,p) X ) assume V is open ; ::_thesis: f " V in D(c,p) X 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 f " V in D(c,p) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A3: ( f is p-continuous & f is (c,p)-continuous ) ; ::_thesis: f is continuous now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_ f_"_V_is_open let V be Subset of Y; ::_thesis: ( V is open implies f " V is open ) assume V is open ; ::_thesis: f " V is open then ( f " V in PO X & f " V in D(c,p) X ) by A3, Def27, Def33; 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; ::_thesis: verum end; hence f is continuous by A1, TOPS_2:43; ::_thesis: verum end; theorem :: DECOMP_1:28 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) ) let f be Function of X,Y; ::_thesis: ( f is continuous iff ( f is ps-continuous & f is (c,ps)-continuous ) ) A1: [#] Y <> {} ; hereby ::_thesis: ( f is ps-continuous & f is (c,ps)-continuous implies f is continuous ) assume A2: f is continuous ; ::_thesis: ( f is ps-continuous & f is (c,ps)-continuous ) thus f is ps-continuous ::_thesis: f is (c,ps)-continuous proof let V be Subset of Y; :: according to DECOMP_1:def_29 ::_thesis: ( V is open implies f " V in PSO X ) assume V is open ; ::_thesis: f " V in PSO X 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 f " V in PSO X by XBOOLE_0:def_4; ::_thesis: verum end; thus f is (c,ps)-continuous ::_thesis: verum proof let V be Subset of Y; :: according to DECOMP_1:def_34 ::_thesis: ( V is open implies f " V in D(c,ps) X ) assume V is open ; ::_thesis: f " V in D(c,ps) X 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 f " V in D(c,ps) X by XBOOLE_0:def_4; ::_thesis: verum end; end; assume A3: ( f is ps-continuous & f is (c,ps)-continuous ) ; ::_thesis: f is continuous now__::_thesis:_for_V_being_Subset_of_Y_st_V_is_open_holds_ f_"_V_is_open let V be Subset of Y; ::_thesis: ( V is open implies f " V is open ) assume V is open ; ::_thesis: f " V is open then ( f " V in PSO X & f " V in D(c,ps) X ) by A3, Def29, Def34; 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; ::_thesis: verum end; hence f is continuous by A1, TOPS_2:43; ::_thesis: verum end;