:: KURATO_1 semantic presentation begin notation let T be non empty TopSpace; let A be Subset of T; synonym A - for Cl A; end; theorem Th1: :: KURATO_1:1 for T being non empty TopSpace for A being Subset of T holds ((((((A -) `) -) `) -) `) - = ((A -) `) - proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ((((((A -) `) -) `) -) `) - = ((A -) `) - let A be Subset of T; ::_thesis: ((((((A -) `) -) `) -) `) - = ((A -) `) - set B = Cl ((Cl A) `); set U = (Cl A) ` ; (Cl A) ` = Int ((Cl A) `) by TOPS_1:23; then (Cl A) ` c= Int (Cl ((Cl A) `)) by PRE_TOPC:18, TOPS_1:19; then ( Cl (Int (Cl ((Cl A) `))) c= Cl (Cl ((Cl A) `)) & Cl ((Cl A) `) c= Cl (Int (Cl ((Cl A) `))) ) by PRE_TOPC:19, TOPS_1:16; then Cl (Int (Cl ((Cl A) `))) = Cl ((Cl A) `) by XBOOLE_0:def_10; hence ((((((A -) `) -) `) -) `) - = ((A -) `) - by TOPS_1:def_1; ::_thesis: verum end; Lm1: for T being 1-sorted for A, B being Subset-Family of T holds A \/ B is Subset-Family of T ; definition let T be non empty TopSpace; let A be Subset of T; func Kurat14Part A -> set equals :: KURATO_1:def 1 {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)}; coherence {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} is set ; end; :: deftheorem defines Kurat14Part KURATO_1:def_1_:_ for T being non empty TopSpace for A being Subset of T holds Kurat14Part A = {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)}; registration let T be non empty TopSpace; let A be Subset of T; cluster Kurat14Part A -> finite ; coherence Kurat14Part A is finite ; end; definition let T be non empty TopSpace; let A be Subset of T; func Kurat14Set A -> Subset-Family of T equals :: KURATO_1:def 2 {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)}; coherence {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T proof set X1 = {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)}; set X2 = {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}; {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} or x in bool the carrier of T ) assume x in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ; ::_thesis: x in bool the carrier of T then ( x = A ` or x = Cl (A `) or x = (Cl (A `)) ` or x = Cl ((Cl (A `)) `) or x = (Cl ((Cl (A `)) `)) ` or x = Cl ((Cl ((Cl (A `)) `)) `) or x = (Cl ((Cl ((Cl (A `)) `)) `)) ` ) by ENUMSET1:def_5; hence x in bool the carrier of T ; ::_thesis: verum end; then reconsider X2 = {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} as Subset-Family of T ; {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} or x in bool the carrier of T ) assume x in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ; ::_thesis: x in bool the carrier of T then ( x = A or x = Cl A or x = (Cl A) ` or x = Cl ((Cl A) `) or x = (Cl ((Cl A) `)) ` or x = Cl ((Cl ((Cl A) `)) `) or x = (Cl ((Cl ((Cl A) `)) `)) ` ) by ENUMSET1:def_5; hence x in bool the carrier of T ; ::_thesis: verum end; then reconsider X1 = {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} as Subset-Family of T ; X1 \/ X2 is Subset-Family of T ; hence {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T ; ::_thesis: verum end; end; :: deftheorem defines Kurat14Set KURATO_1:def_2_:_ for T being non empty TopSpace for A being Subset of T holds Kurat14Set A = {A,(A -),((A -) `),(((A -) `) -),((((A -) `) -) `),(((((A -) `) -) `) -),((((((A -) `) -) `) -) `)} \/ {(A `),((A `) -),(((A `) -) `),((((A `) -) `) -),(((((A `) -) `) -) `),((((((A `) -) `) -) `) -),(((((((A `) -) `) -) `) -) `)}; theorem :: KURATO_1:2 for T being non empty TopSpace for A being Subset of T holds Kurat14Set A = (Kurat14Part A) \/ (Kurat14Part (A `)) ; theorem Th3: :: KURATO_1:3 for T being non empty TopSpace for A being Subset of T holds ( A in Kurat14Set A & A - in Kurat14Set A & (A -) ` in Kurat14Set A & ((A -) `) - in Kurat14Set A & (((A -) `) -) ` in Kurat14Set A & ((((A -) `) -) `) - in Kurat14Set A & (((((A -) `) -) `) -) ` in Kurat14Set A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A in Kurat14Set A & A - in Kurat14Set A & (A -) ` in Kurat14Set A & ((A -) `) - in Kurat14Set A & (((A -) `) -) ` in Kurat14Set A & ((((A -) `) -) `) - in Kurat14Set A & (((((A -) `) -) `) -) ` in Kurat14Set A ) let A be Subset of T; ::_thesis: ( A in Kurat14Set A & A - in Kurat14Set A & (A -) ` in Kurat14Set A & ((A -) `) - in Kurat14Set A & (((A -) `) -) ` in Kurat14Set A & ((((A -) `) -) `) - in Kurat14Set A & (((((A -) `) -) `) -) ` in Kurat14Set A ) A1: ( Cl A in Kurat14Part A & (Cl A) ` in Kurat14Part A ) by ENUMSET1:def_5; A2: ( Cl ((Cl A) `) in Kurat14Part A & (Cl ((Cl A) `)) ` in Kurat14Part A ) by ENUMSET1:def_5; A3: ( Cl ((Cl ((Cl A) `)) `) in Kurat14Part A & (Cl ((Cl ((Cl A) `)) `)) ` in Kurat14Part A ) by ENUMSET1:def_5; ( Kurat14Part A c= Kurat14Set A & A in Kurat14Part A ) by ENUMSET1:def_5, XBOOLE_1:7; hence ( A in Kurat14Set A & A - in Kurat14Set A & (A -) ` in Kurat14Set A & ((A -) `) - in Kurat14Set A & (((A -) `) -) ` in Kurat14Set A & ((((A -) `) -) `) - in Kurat14Set A & (((((A -) `) -) `) -) ` in Kurat14Set A ) by A1, A2, A3; ::_thesis: verum end; theorem Th4: :: KURATO_1:4 for T being non empty TopSpace for A being Subset of T holds ( A ` in Kurat14Set A & (A `) - in Kurat14Set A & ((A `) -) ` in Kurat14Set A & (((A `) -) `) - in Kurat14Set A & ((((A `) -) `) -) ` in Kurat14Set A & (((((A `) -) `) -) `) - in Kurat14Set A & ((((((A `) -) `) -) `) -) ` in Kurat14Set A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A ` in Kurat14Set A & (A `) - in Kurat14Set A & ((A `) -) ` in Kurat14Set A & (((A `) -) `) - in Kurat14Set A & ((((A `) -) `) -) ` in Kurat14Set A & (((((A `) -) `) -) `) - in Kurat14Set A & ((((((A `) -) `) -) `) -) ` in Kurat14Set A ) let A be Subset of T; ::_thesis: ( A ` in Kurat14Set A & (A `) - in Kurat14Set A & ((A `) -) ` in Kurat14Set A & (((A `) -) `) - in Kurat14Set A & ((((A `) -) `) -) ` in Kurat14Set A & (((((A `) -) `) -) `) - in Kurat14Set A & ((((((A `) -) `) -) `) -) ` in Kurat14Set A ) A1: ( Cl (A `) in Kurat14Part (A `) & (Cl (A `)) ` in Kurat14Part (A `) ) by ENUMSET1:def_5; A2: ( Cl ((Cl (A `)) `) in Kurat14Part (A `) & (Cl ((Cl (A `)) `)) ` in Kurat14Part (A `) ) by ENUMSET1:def_5; A3: ( Cl ((Cl ((Cl (A `)) `)) `) in Kurat14Part (A `) & (Cl ((Cl ((Cl (A `)) `)) `)) ` in Kurat14Part (A `) ) by ENUMSET1:def_5; ( Kurat14Part (A `) c= Kurat14Set A & A ` in Kurat14Part (A `) ) by ENUMSET1:def_5, XBOOLE_1:7; hence ( A ` in Kurat14Set A & (A `) - in Kurat14Set A & ((A `) -) ` in Kurat14Set A & (((A `) -) `) - in Kurat14Set A & ((((A `) -) `) -) ` in Kurat14Set A & (((((A `) -) `) -) `) - in Kurat14Set A & ((((((A `) -) `) -) `) -) ` in Kurat14Set A ) by A1, A2, A3; ::_thesis: verum end; definition let T be non empty TopSpace; let A be Subset of T; func Kurat14ClPart A -> Subset-Family of T equals :: KURATO_1:def 3 {(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)}; coherence {(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)} is Subset-Family of T proof A1: {(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} is Subset-Family of T by MEASURE1:3; ( {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} = {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `))} \/ {(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} & {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `))} is Subset-Family of T ) by ENUMSET1:13, MEASURE1:3; hence {(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)} is Subset-Family of T by A1, Lm1; ::_thesis: verum end; func Kurat14OpPart A -> Subset-Family of T equals :: KURATO_1:def 4 {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)}; coherence {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T proof A2: {((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} is Subset-Family of T by MEASURE1:3; ( {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} = {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `)} \/ {((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `)} is Subset-Family of T ) by ENUMSET1:13, MEASURE1:3; hence {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)} is Subset-Family of T by A2, Lm1; ::_thesis: verum end; end; :: deftheorem defines Kurat14ClPart KURATO_1:def_3_:_ for T being non empty TopSpace for A being Subset of T holds Kurat14ClPart A = {(A -),(((A -) `) -),(((((A -) `) -) `) -),((A `) -),((((A `) -) `) -),((((((A `) -) `) -) `) -)}; :: deftheorem defines Kurat14OpPart KURATO_1:def_4_:_ for T being non empty TopSpace for A being Subset of T holds Kurat14OpPart A = {((A -) `),((((A -) `) -) `),((((((A -) `) -) `) -) `),(((A `) -) `),(((((A `) -) `) -) `),(((((((A `) -) `) -) `) -) `)}; Lm2: for T being non empty TopSpace for A being Subset of T holds Kurat14Set A = ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds Kurat14Set A = ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} let A be Subset of T; ::_thesis: Kurat14Set A = ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} set Y1 = {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))}; set Y2 = {A,(A `)}; set Y3 = {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)}; set Y = ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)}; A1: {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} c= ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by XBOOLE_1:7; A2: ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} c= Kurat14Set A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} or x in Kurat14Set A ) assume x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ; ::_thesis: x in Kurat14Set A then A3: ( x in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)} or x in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by XBOOLE_0:def_3; percases ( x in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} or x in {A,(A `)} or x in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by A3, XBOOLE_0:def_3; suppose x in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} ; ::_thesis: x in Kurat14Set A then ( x = Cl A or x = Cl ((Cl A) `) or x = Cl ((Cl ((Cl A) `)) `) or x = Cl (A `) or x = Cl ((Cl (A `)) `) or x = Cl ((Cl ((Cl (A `)) `)) `) ) by ENUMSET1:def_4; hence x in Kurat14Set A by Th3, Th4; ::_thesis: verum end; suppose x in {A,(A `)} ; ::_thesis: x in Kurat14Set A then ( x = A or x = A ` ) by TARSKI:def_2; hence x in Kurat14Set A by Th3, Th4; ::_thesis: verum end; suppose x in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ; ::_thesis: x in Kurat14Set A then ( x = (Cl A) ` or x = (Cl ((Cl A) `)) ` or x = (Cl ((Cl ((Cl A) `)) `)) ` or x = (Cl (A `)) ` or x = (Cl ((Cl (A `)) `)) ` or x = (Cl ((Cl ((Cl (A `)) `)) `)) ` ) by ENUMSET1:def_4; hence x in Kurat14Set A by Th3, Th4; ::_thesis: verum end; end; end; A4: {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)} c= ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by XBOOLE_1:7; (Cl ((Cl A) `)) ` in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by ENUMSET1:def_4; then A5: (Cl ((Cl A) `)) ` in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A1; (Cl A) ` in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by ENUMSET1:def_4; then A6: (Cl A) ` in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A1; {A,(A `)} c= {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)} by XBOOLE_1:7; then A7: {A,(A `)} c= ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A4, XBOOLE_1:1; (Cl ((Cl ((Cl (A `)) `)) `)) ` in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by ENUMSET1:def_4; then A8: (Cl ((Cl ((Cl (A `)) `)) `)) ` in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A1; (Cl ((Cl (A `)) `)) ` in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by ENUMSET1:def_4; then A9: (Cl ((Cl (A `)) `)) ` in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A1; (Cl (A `)) ` in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by ENUMSET1:def_4; then A10: (Cl (A `)) ` in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A1; (Cl ((Cl ((Cl A) `)) `)) ` in {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by ENUMSET1:def_4; then A11: (Cl ((Cl ((Cl A) `)) `)) ` in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A1; A in {A,(A `)} by TARSKI:def_2; then A12: A in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A7; {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} c= {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)} by XBOOLE_1:7; then A13: {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} c= ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A4, XBOOLE_1:1; A ` in {A,(A `)} by TARSKI:def_2; then A14: A ` in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A7; Cl ((Cl ((Cl (A `)) `)) `) in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} by ENUMSET1:def_4; then A15: Cl ((Cl ((Cl (A `)) `)) `) in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A13; Cl ((Cl (A `)) `) in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} by ENUMSET1:def_4; then A16: Cl ((Cl (A `)) `) in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A13; Cl (A `) in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} by ENUMSET1:def_4; then A17: Cl (A `) in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A13; Cl ((Cl ((Cl A) `)) `) in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} by ENUMSET1:def_4; then A18: Cl ((Cl ((Cl A) `)) `) in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A13; Cl ((Cl A) `) in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} by ENUMSET1:def_4; then A19: Cl ((Cl A) `) in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A13; Cl A in {(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} by ENUMSET1:def_4; then A20: Cl A in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A13; Kurat14Set A c= ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Kurat14Set A or x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) assume A21: x in Kurat14Set A ; ::_thesis: x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} percases ( x in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} or x in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by A21, XBOOLE_0:def_3; suppose x in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ; ::_thesis: x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} hence x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A20, A19, A18, A12, A6, A5, A11, ENUMSET1:def_5; ::_thesis: verum end; suppose x in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ; ::_thesis: x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} hence x in ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A17, A16, A15, A14, A10, A9, A8, ENUMSET1:def_5; ::_thesis: verum end; end; end; hence Kurat14Set A = ({(Cl A),(Cl ((Cl A) `)),(Cl ((Cl ((Cl A) `)) `)),(Cl (A `)),(Cl ((Cl (A `)) `)),(Cl ((Cl ((Cl (A `)) `)) `))} \/ {A,(A `)}) \/ {((Cl A) `),((Cl ((Cl A) `)) `),((Cl ((Cl ((Cl A) `)) `)) `),((Cl (A `)) `),((Cl ((Cl (A `)) `)) `),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: KURATO_1:5 for T being non empty TopSpace for A being Subset of T holds Kurat14Set A = ({A,(A `)} \/ (Kurat14ClPart A)) \/ (Kurat14OpPart A) by Lm2; registration let T be non empty TopSpace; let A be Subset of T; cluster Kurat14Set A -> finite ; coherence Kurat14Set A is finite ; end; theorem Th6: :: KURATO_1:6 for T being non empty TopSpace for A, Q being Subset of T st Q in Kurat14Set A holds ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) proof let T be non empty TopSpace; ::_thesis: for A, Q being Subset of T st Q in Kurat14Set A holds ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) let A, Q be Subset of T; ::_thesis: ( Q in Kurat14Set A implies ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) ) set k1 = Cl A; set k2 = (Cl A) ` ; set k3 = Cl ((Cl A) `); set k4 = (Cl ((Cl A) `)) ` ; set k5 = Cl ((Cl ((Cl A) `)) `); set k6 = (Cl ((Cl ((Cl A) `)) `)) ` ; set k7 = Cl (A `); set k8 = (Cl (A `)) ` ; set k9 = Cl ((Cl (A `)) `); set k10 = (Cl ((Cl (A `)) `)) ` ; set k11 = Cl ((Cl ((Cl (A `)) `)) `); set k12 = (Cl ((Cl ((Cl (A `)) `)) `)) ` ; assume A1: Q in Kurat14Set A ; ::_thesis: ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) percases ( Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} or Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by A1, XBOOLE_0:def_3; supposeA2: Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ; ::_thesis: ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) proof percases ( Q = A or Q = Cl A or Q = (Cl A) ` or Q = Cl ((Cl A) `) or Q = (Cl ((Cl A) `)) ` or Q = Cl ((Cl ((Cl A) `)) `) or Q = (Cl ((Cl ((Cl A) `)) `)) ` ) by A2, ENUMSET1:def_5; suppose Q = A ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} & Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = Cl A ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} & Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = (Cl A) ` ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} & Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = Cl ((Cl A) `) ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} & Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = (Cl ((Cl A) `)) ` ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} & Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = Cl ((Cl ((Cl A) `)) `) ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} & Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA3: Q = (Cl ((Cl ((Cl A) `)) `)) ` ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) Cl ((Cl ((Cl ((Cl A) `)) `)) `) = Cl ((Cl A) `) by Th1; then A4: Cl Q in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} by A3, ENUMSET1:def_5; Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} by A3, ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by A4, XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) ; ::_thesis: verum end; supposeA5: Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ; ::_thesis: ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) proof percases ( Q = A ` or Q = Cl (A `) or Q = (Cl (A `)) ` or Q = Cl ((Cl (A `)) `) or Q = (Cl ((Cl (A `)) `)) ` or Q = Cl ((Cl ((Cl (A `)) `)) `) or Q = (Cl ((Cl ((Cl (A `)) `)) `)) ` ) by A5, ENUMSET1:def_5; suppose Q = A ` ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & Q ` in {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = Cl (A `) ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = (Cl (A `)) ` ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = Cl ((Cl (A `)) `) ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = (Cl ((Cl (A `)) `)) ` ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; suppose Q = Cl ((Cl ((Cl (A `)) `)) `) ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then ( Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} & Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} ) by ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA6: Q = (Cl ((Cl ((Cl (A `)) `)) `)) ` ; ::_thesis: ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) then Cl Q = Cl ((Cl (A `)) `) by Th1; then A7: Cl Q in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by ENUMSET1:def_5; Q ` in {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} by A6, ENUMSET1:def_5; hence ( Q ` in Kurat14Set A & Cl Q in Kurat14Set A ) by A7, XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence ( Q ` in Kurat14Set A & Q - in Kurat14Set A ) ; ::_thesis: verum end; end; end; theorem :: KURATO_1:7 for T being non empty TopSpace for A being Subset of T holds card (Kurat14Set A) <= 14 proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds card (Kurat14Set A) <= 14 let A be Subset of T; ::_thesis: card (Kurat14Set A) <= 14 set X = {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)}; set Y = {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}; ( card {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} <= 7 & card {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)} <= 7 ) by CARD_2:55; then ( card ({A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)} \/ {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}) <= (card {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)}) + (card {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}) & (card {A,(Cl A),((Cl A) `),(Cl ((Cl A) `)),((Cl ((Cl A) `)) `),(Cl ((Cl ((Cl A) `)) `)),((Cl ((Cl ((Cl A) `)) `)) `)}) + (card {(A `),(Cl (A `)),((Cl (A `)) `),(Cl ((Cl (A `)) `)),((Cl ((Cl (A `)) `)) `),(Cl ((Cl ((Cl (A `)) `)) `)),((Cl ((Cl ((Cl (A `)) `)) `)) `)}) <= 7 + 7 ) by CARD_2:43, XREAL_1:7; hence card (Kurat14Set A) <= 14 by XXREAL_0:2; ::_thesis: verum end; begin definition let T be non empty TopSpace; let A be Subset of T; func Kurat7Set A -> Subset-Family of T equals :: KURATO_1:def 5 {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))}; coherence {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} is Subset-Family of T proof set X = {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))}; {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} or x in bool the carrier of T ) assume x in {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} ; ::_thesis: x in bool the carrier of T then ( x = A or x = Int A or x = Cl A or x = Int (Cl A) or x = Cl (Int A) or x = Cl (Int (Cl A)) or x = Int (Cl (Int A)) ) by ENUMSET1:def_5; hence x in bool the carrier of T ; ::_thesis: verum end; hence {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} is Subset-Family of T ; ::_thesis: verum end; end; :: deftheorem defines Kurat7Set KURATO_1:def_5_:_ for T being non empty TopSpace for A being Subset of T holds Kurat7Set A = {A,(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))}; theorem :: KURATO_1:8 for T being non empty TopSpace for A being Subset of T holds Kurat7Set A = ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))} proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds Kurat7Set A = ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))} let A be Subset of T; ::_thesis: Kurat7Set A = ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))} Kurat7Set A = {A} \/ {(Int A),(Cl A),(Int (Cl A)),(Cl (Int A)),(Cl (Int (Cl A))),(Int (Cl (Int A)))} by ENUMSET1:16 .= {A} \/ ({(Int A),(Int (Cl A)),(Int (Cl (Int A)))} \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))}) by BORSUK_5:2 .= ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))} by XBOOLE_1:4 ; hence Kurat7Set A = ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))} ; ::_thesis: verum end; registration let T be non empty TopSpace; let A be Subset of T; cluster Kurat7Set A -> finite ; coherence Kurat7Set A is finite ; end; theorem Th9: :: KURATO_1:9 for T being non empty TopSpace for A, Q being Subset of T st Q in Kurat7Set A holds ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) proof let T be non empty TopSpace; ::_thesis: for A, Q being Subset of T st Q in Kurat7Set A holds ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) let A, Q be Subset of T; ::_thesis: ( Q in Kurat7Set A implies ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) ) assume A1: Q in Kurat7Set A ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) proof percases ( Q = A or Q = Int A or Q = Cl A or Q = Int (Cl A) or Q = Cl (Int A) or Q = Cl (Int (Cl A)) or Q = Int (Cl (Int A)) ) by A1, ENUMSET1:def_5; suppose Q = A ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def_5; ::_thesis: verum end; suppose Q = Int A ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def_5; ::_thesis: verum end; suppose Q = Cl A ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def_5; ::_thesis: verum end; suppose Q = Int (Cl A) ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def_5; ::_thesis: verum end; suppose Q = Cl (Int A) ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def_5; ::_thesis: verum end; supposeA2: Q = Cl (Int (Cl A)) ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) Int (Cl (Int (Cl A))) = Int (Cl A) by TDLAT_1:5; hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by A2, ENUMSET1:def_5; ::_thesis: verum end; supposeA3: Q = Int (Cl (Int A)) ; ::_thesis: ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) then Cl Q = Cl (Int A) by TOPS_1:26; hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by A3, ENUMSET1:def_5; ::_thesis: verum end; end; end; hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) ; ::_thesis: verum end; begin definition func KurExSet -> Subset of R^1 equals :: KURATO_1:def 6 (({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[; coherence (({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[ is Subset of R^1 by TOPMETR:17; end; :: deftheorem defines KurExSet KURATO_1:def_6_:_ KurExSet = (({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[; theorem Th10: :: KURATO_1:10 Cl KurExSet = {1} \/ [.2,+infty.[ proof set A = KurExSet ; reconsider B = {1}, C = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ as Subset of R^1 by TOPMETR:17; KurExSet = {1} \/ (((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[) by XBOOLE_1:113; then A1: Cl KurExSet = (Cl B) \/ (Cl C) by PRE_TOPC:20; Cl B = {1} by BORSUK_5:38; hence Cl KurExSet = {1} \/ [.2,+infty.[ by A1, BORSUK_5:56; ::_thesis: verum end; theorem Th11: :: KURATO_1:11 (Cl KurExSet) ` = ].-infty,1.[ \/ ].1,2.[ by Th10, BORSUK_5:63; theorem Th12: :: KURATO_1:12 Cl ((Cl KurExSet) `) = ].-infty,2.] by Th11, BORSUK_5:64; theorem Th13: :: KURATO_1:13 (Cl ((Cl KurExSet) `)) ` = ].2,+infty.[ by Th12, TOPMETR:17, XXREAL_1:224, XXREAL_1:288; theorem Th14: :: KURATO_1:14 Cl ((Cl ((Cl KurExSet) `)) `) = [.2,+infty.[ by Th13, BORSUK_5:49; theorem Th15: :: KURATO_1:15 (Cl ((Cl ((Cl KurExSet) `)) `)) ` = ].-infty,2.[ by Th14, TOPMETR:17, XXREAL_1:224, XXREAL_1:294; theorem Th16: :: KURATO_1:16 KurExSet ` = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5} proof set A = KurExSet ; reconsider B = {1}, C = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ as Subset of R^1 by TOPMETR:17; A1: C ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} by BORSUK_5:60; ( KurExSet = {1} \/ (((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[) & B ` = ].-infty,1.[ \/ ].1,+infty.[ ) by BORSUK_5:61, XBOOLE_1:113; hence KurExSet ` = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5} by A1, BORSUK_5:62, XBOOLE_1:53; ::_thesis: verum end; theorem Th17: :: KURATO_1:17 Cl (KurExSet `) = ].-infty,4.] \/ {5} by Th16, BORSUK_5:67; theorem Th18: :: KURATO_1:18 (Cl (KurExSet `)) ` = ].4,5.[ \/ ].5,+infty.[ by Th17, BORSUK_5:68; theorem Th19: :: KURATO_1:19 Cl ((Cl (KurExSet `)) `) = [.4,+infty.[ by Th18, BORSUK_5:55; theorem Th20: :: KURATO_1:20 (Cl ((Cl (KurExSet `)) `)) ` = ].-infty,4.[ by Th19, TOPMETR:17, XXREAL_1:224, XXREAL_1:294; theorem Th21: :: KURATO_1:21 Cl ((Cl ((Cl (KurExSet `)) `)) `) = ].-infty,4.] by Th20, BORSUK_5:51; theorem Th22: :: KURATO_1:22 (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` = ].4,+infty.[ by Th21, TOPMETR:17, XXREAL_1:224, XXREAL_1:288; begin theorem Th23: :: KURATO_1:23 Int KurExSet = ].4,5.[ \/ ].5,+infty.[ by Th18, TOPS_1:def_1; theorem Th24: :: KURATO_1:24 Cl (Int KurExSet) = [.4,+infty.[ by Th18, BORSUK_5:55, TOPS_1:def_1; theorem Th25: :: KURATO_1:25 Int (Cl (Int KurExSet)) = ].4,+infty.[ proof set A = KurExSet ; Cl (Int KurExSet) = Cl ((Cl (KurExSet `)) `) by TOPS_1:def_1; then A1: Int (Cl (Int KurExSet)) = (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` by TOPS_1:def_1; (Cl ((Cl (KurExSet `)) `)) ` = ].-infty,4.[ by Th19, TOPMETR:17, XXREAL_1:224, XXREAL_1:294; then Cl ((Cl ((Cl (KurExSet `)) `)) `) = ].-infty,4.] by BORSUK_5:51; hence Int (Cl (Int KurExSet)) = ].4,+infty.[ by A1, TOPMETR:17, XXREAL_1:224, XXREAL_1:288; ::_thesis: verum end; theorem Th26: :: KURATO_1:26 Int (Cl KurExSet) = ].2,+infty.[ proof set A = KurExSet ; (Cl KurExSet) ` = ].-infty,1.[ \/ ].1,2.[ by Th10, BORSUK_5:63; then Cl ((Cl KurExSet) `) = ].-infty,2.] by BORSUK_5:64; then (Cl ((Cl KurExSet) `)) ` = ].2,+infty.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:288; hence Int (Cl KurExSet) = ].2,+infty.[ by TOPS_1:def_1; ::_thesis: verum end; theorem Th27: :: KURATO_1:27 Cl (Int (Cl KurExSet)) = [.2,+infty.[ proof set A = KurExSet ; (Cl KurExSet) ` = ].-infty,1.[ \/ ].1,2.[ by Th10, BORSUK_5:63; then Cl ((Cl KurExSet) `) = ].-infty,2.] by BORSUK_5:64; then (Cl ((Cl KurExSet) `)) ` = ].2,+infty.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:288; hence Cl (Int (Cl KurExSet)) = [.2,+infty.[ by BORSUK_5:49, TOPS_1:def_1; ::_thesis: verum end; begin theorem :: KURATO_1:28 Cl (Int (Cl KurExSet)) <> Int (Cl KurExSet) proof set A = KurExSet ; 2 in Cl (Int (Cl KurExSet)) by Th27, XXREAL_1:236; hence Cl (Int (Cl KurExSet)) <> Int (Cl KurExSet) by Th26, XXREAL_1:235; ::_thesis: verum end; theorem Th29: :: KURATO_1:29 Cl (Int (Cl KurExSet)) <> Cl KurExSet proof set A = KurExSet ; 1 in {1} by TARSKI:def_1; then 1 in Cl KurExSet by Th10, XBOOLE_0:def_3; hence Cl (Int (Cl KurExSet)) <> Cl KurExSet by Th27, XXREAL_1:236; ::_thesis: verum end; theorem :: KURATO_1:30 Cl (Int (Cl KurExSet)) <> Int (Cl (Int KurExSet)) proof set A = KurExSet ; 3 in Cl (Int (Cl KurExSet)) by Th27, XXREAL_1:236; hence Cl (Int (Cl KurExSet)) <> Int (Cl (Int KurExSet)) by Th25, XXREAL_1:235; ::_thesis: verum end; theorem Th31: :: KURATO_1:31 Cl (Int (Cl KurExSet)) <> Cl (Int KurExSet) proof set A = KurExSet ; 2 in Cl (Int (Cl KurExSet)) by Th27, XXREAL_1:236; hence Cl (Int (Cl KurExSet)) <> Cl (Int KurExSet) by Th24, XXREAL_1:236; ::_thesis: verum end; theorem :: KURATO_1:32 Cl (Int (Cl KurExSet)) <> Int KurExSet proof set A = KurExSet ; ( 2 in Cl (Int (Cl KurExSet)) & Int KurExSet = ].4,5.[ \/ ].5,+infty.[ ) by Th18, Th27, TOPS_1:def_1, XXREAL_1:236; hence Cl (Int (Cl KurExSet)) <> Int KurExSet by XXREAL_1:223; ::_thesis: verum end; theorem :: KURATO_1:33 Int (Cl KurExSet) <> Cl KurExSet proof set A = KurExSet ; 1 in {1} by TARSKI:def_1; then 1 in Cl KurExSet by Th10, XBOOLE_0:def_3; hence Int (Cl KurExSet) <> Cl KurExSet by Th26, XXREAL_1:235; ::_thesis: verum end; theorem :: KURATO_1:34 Int (Cl KurExSet) <> Int (Cl (Int KurExSet)) proof set A = KurExSet ; 3 in Int (Cl KurExSet) by Th26, XXREAL_1:235; hence Int (Cl KurExSet) <> Int (Cl (Int KurExSet)) by Th25, XXREAL_1:235; ::_thesis: verum end; theorem :: KURATO_1:35 Int (Cl KurExSet) <> Cl (Int KurExSet) by Th26, BORSUK_5:34, BORSUK_5:45; theorem Th36: :: KURATO_1:36 Int (Cl KurExSet) <> Int KurExSet proof set A = KurExSet ; ( 5 in Int (Cl KurExSet) & Int KurExSet = ].4,5.[ \/ ].5,+infty.[ ) by Th18, Th26, TOPS_1:def_1, XXREAL_1:235; hence Int (Cl KurExSet) <> Int KurExSet by XXREAL_1:205; ::_thesis: verum end; theorem :: KURATO_1:37 Int (Cl (Int KurExSet)) <> Cl KurExSet proof set A = KurExSet ; 2 in [.2,+infty.[ by XXREAL_1:236; then 2 in Cl KurExSet by Th10, XBOOLE_0:def_3; hence Int (Cl (Int KurExSet)) <> Cl KurExSet by Th25, XXREAL_1:235; ::_thesis: verum end; theorem Th38: :: KURATO_1:38 Cl (Int KurExSet) <> Cl KurExSet proof set A = KurExSet ; 2 in [.2,+infty.[ by XXREAL_1:236; then 2 in Cl KurExSet by Th10, XBOOLE_0:def_3; hence Cl (Int KurExSet) <> Cl KurExSet by Th24, XXREAL_1:236; ::_thesis: verum end; theorem :: KURATO_1:39 Int KurExSet <> Cl KurExSet proof set A = KurExSet ; 5 in [.2,+infty.[ by XXREAL_1:236; then A1: 5 in Cl KurExSet by Th10, XBOOLE_0:def_3; Int KurExSet = ].4,5.[ \/ ].5,+infty.[ by Th18, TOPS_1:def_1; hence Int KurExSet <> Cl KurExSet by A1, XXREAL_1:205; ::_thesis: verum end; theorem Th40: :: KURATO_1:40 Cl KurExSet <> KurExSet proof set A = KurExSet ; ( not 5 in {1} & not 5 in RAT (2,4) ) by BORSUK_5:29, TARSKI:def_1; then ( not 5 in ].4,5.[ & not 5 in {1} \/ (RAT (2,4)) ) by XBOOLE_0:def_3, XXREAL_1:4; then A1: ( not 5 in ].5,+infty.[ & not 5 in ({1} \/ (RAT (2,4))) \/ ].4,5.[ ) by XBOOLE_0:def_3, XXREAL_1:235; 5 in [.2,+infty.[ by XXREAL_1:236; then 5 in Cl KurExSet by Th10, XBOOLE_0:def_3; hence Cl KurExSet <> KurExSet by A1, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th41: :: KURATO_1:41 KurExSet <> Int KurExSet proof set A = KurExSet ; 1 in {1} by TARSKI:def_1; then 1 in {1} \/ (RAT (2,4)) by XBOOLE_0:def_3; then 1 in ({1} \/ (RAT (2,4))) \/ ].4,5.[ by XBOOLE_0:def_3; then A1: 1 in KurExSet by XBOOLE_0:def_3; Int KurExSet = ].4,5.[ \/ ].5,+infty.[ by Th18, TOPS_1:def_1; hence KurExSet <> Int KurExSet by A1, XXREAL_1:223; ::_thesis: verum end; theorem :: KURATO_1:42 Cl (Int KurExSet) <> Int (Cl (Int KurExSet)) proof set A = KurExSet ; 4 in Cl (Int KurExSet) by Th24, XXREAL_1:236; hence Cl (Int KurExSet) <> Int (Cl (Int KurExSet)) by Th25, XXREAL_1:235; ::_thesis: verum end; theorem Th43: :: KURATO_1:43 Int (Cl (Int KurExSet)) <> Int KurExSet proof set A = KurExSet ; ( 5 in Int (Cl (Int KurExSet)) & Int KurExSet = ].4,5.[ \/ ].5,+infty.[ ) by Th18, Th25, TOPS_1:def_1, XXREAL_1:235; hence Int (Cl (Int KurExSet)) <> Int KurExSet by XXREAL_1:205; ::_thesis: verum end; theorem :: KURATO_1:44 Cl (Int KurExSet) <> Int KurExSet proof set A = KurExSet ; ( 4 in Cl (Int KurExSet) & Int KurExSet = ].4,5.[ \/ ].5,+infty.[ ) by Th18, Th24, TOPS_1:def_1, XXREAL_1:236; hence Cl (Int KurExSet) <> Int KurExSet by XXREAL_1:223; ::_thesis: verum end; begin theorem Th45: :: KURATO_1:45 Int (Cl (Int KurExSet)) <> Int (Cl KurExSet) proof set A = KurExSet ; not 3 in Int (Cl (Int KurExSet)) by Th25, XXREAL_1:235; hence Int (Cl (Int KurExSet)) <> Int (Cl KurExSet) by Th26, XXREAL_1:235; ::_thesis: verum end; theorem Th46: :: KURATO_1:46 Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)) are_mutually_different proof set A1 = Int KurExSet; set A2 = Int (Cl KurExSet); set A3 = Int (Cl (Int KurExSet)); thus Int KurExSet <> Int (Cl KurExSet) by Th36; :: according to ZFMISC_1:def_5 ::_thesis: ( not Int KurExSet = Int (Cl (Int KurExSet)) & not Int (Cl KurExSet) = Int (Cl (Int KurExSet)) ) thus Int KurExSet <> Int (Cl (Int KurExSet)) by Th43; ::_thesis: not Int (Cl KurExSet) = Int (Cl (Int KurExSet)) thus not Int (Cl KurExSet) = Int (Cl (Int KurExSet)) by Th45; ::_thesis: verum end; theorem Th47: :: KURATO_1:47 Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different proof set A1 = Cl KurExSet; set A2 = Cl (Int KurExSet); set A3 = Cl (Int (Cl KurExSet)); thus Cl KurExSet <> Cl (Int KurExSet) by Th38; :: according to ZFMISC_1:def_5 ::_thesis: ( not Cl KurExSet = Cl (Int (Cl KurExSet)) & not Cl (Int KurExSet) = Cl (Int (Cl KurExSet)) ) thus Cl KurExSet <> Cl (Int (Cl KurExSet)) by Th29; ::_thesis: not Cl (Int KurExSet) = Cl (Int (Cl KurExSet)) thus not Cl (Int KurExSet) = Cl (Int (Cl KurExSet)) by Th31; ::_thesis: verum end; theorem Th48: :: KURATO_1:48 for X being set st X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} holds X is non empty open Subset of R^1 proof let X be set ; ::_thesis: ( X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} implies X is non empty open Subset of R^1 ) assume A1: X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} ; ::_thesis: X is non empty open Subset of R^1 percases ( X = Int KurExSet or X = Int (Cl KurExSet) or X = Int (Cl (Int KurExSet)) ) by A1, ENUMSET1:def_1; suppose X = Int KurExSet ; ::_thesis: X is non empty open Subset of R^1 hence X is non empty open Subset of R^1 by Th18, TOPS_1:def_1; ::_thesis: verum end; suppose X = Int (Cl KurExSet) ; ::_thesis: X is non empty open Subset of R^1 hence X is non empty open Subset of R^1 by Th26; ::_thesis: verum end; suppose X = Int (Cl (Int KurExSet)) ; ::_thesis: X is non empty open Subset of R^1 hence X is non empty open Subset of R^1 by Th25; ::_thesis: verum end; end; end; theorem Th49: :: KURATO_1:49 for X being set st X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} holds X <> REAL proof let X be set ; ::_thesis: ( X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} implies X <> REAL ) assume A1: X in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} ; ::_thesis: X <> REAL percases ( X = Int KurExSet or X = Int (Cl KurExSet) or X = Int (Cl (Int KurExSet)) ) by A1, ENUMSET1:def_1; suppose X = Int KurExSet ; ::_thesis: X <> REAL hence X <> REAL by Th23, XXREAL_1:205; ::_thesis: verum end; suppose X = Int (Cl KurExSet) ; ::_thesis: X <> REAL hence X <> REAL by Th26, BORSUK_5:45; ::_thesis: verum end; suppose X = Int (Cl (Int KurExSet)) ; ::_thesis: X <> REAL hence X <> REAL by Th25, BORSUK_5:45; ::_thesis: verum end; end; end; theorem :: KURATO_1:50 for X being set st X in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} holds X <> REAL proof let X be set ; ::_thesis: ( X in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} implies X <> REAL ) assume A1: X in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} ; ::_thesis: X <> REAL percases ( X = Cl KurExSet or X = Cl (Int KurExSet) or X = Cl (Int (Cl KurExSet)) ) by A1, ENUMSET1:def_1; supposeA2: X = Cl KurExSet ; ::_thesis: X <> REAL ( not 0 in {1} & not 0 in [.2,+infty.[ ) by XXREAL_1:236; hence X <> REAL by A2, Th10, XBOOLE_0:def_3; ::_thesis: verum end; suppose X = Cl (Int KurExSet) ; ::_thesis: X <> REAL hence X <> REAL by Th24, BORSUK_5:46; ::_thesis: verum end; suppose X = Cl (Int (Cl KurExSet)) ; ::_thesis: X <> REAL hence X <> REAL by Th27, BORSUK_5:46; ::_thesis: verum end; end; end; theorem Th51: :: KURATO_1:51 {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} misses {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} proof set X = {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))}; set Y = {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))}; assume {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} meets {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} ; ::_thesis: contradiction then consider x being set such that A1: x in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet)))} and A2: x in {(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} by XBOOLE_0:3; ( x is non empty open Subset of R^1 & x is closed Subset of R^1 ) by A1, A2, Th48, ENUMSET1:def_1; hence contradiction by A1, Th49, BORSUK_5:34; ::_thesis: verum end; theorem Th52: :: KURATO_1:52 Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different by Th46, Th47, Th51, BORSUK_5:6; registration cluster KurExSet -> non open non closed ; coherence ( not KurExSet is closed & not KurExSet is open ) by Th40, Th41, PRE_TOPC:22, TOPS_1:23; end; theorem Th53: :: KURATO_1:53 {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet))),(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} misses {KurExSet} proof set A = KurExSet ; assume {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet))),(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} meets {KurExSet} ; ::_thesis: contradiction then A1: KurExSet in {(Int KurExSet),(Int (Cl KurExSet)),(Int (Cl (Int KurExSet))),(Cl KurExSet),(Cl (Int KurExSet)),(Cl (Int (Cl KurExSet)))} by ZFMISC_1:50; percases ( KurExSet = Int KurExSet or KurExSet = Int (Cl KurExSet) or KurExSet = Int (Cl (Int KurExSet)) or KurExSet = Cl KurExSet or KurExSet = Cl (Int KurExSet) or KurExSet = Cl (Int (Cl KurExSet)) ) by A1, ENUMSET1:def_4; suppose KurExSet = Int KurExSet ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; suppose KurExSet = Int (Cl KurExSet) ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; suppose KurExSet = Int (Cl (Int KurExSet)) ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; suppose KurExSet = Cl KurExSet ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; suppose KurExSet = Cl (Int KurExSet) ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; suppose KurExSet = Cl (Int (Cl KurExSet)) ; ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; end; end; theorem Th54: :: KURATO_1:54 KurExSet , Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different proof Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)), KurExSet are_mutually_different by Th52, Th53, BORSUK_5:7; hence KurExSet , Int KurExSet, Int (Cl KurExSet), Int (Cl (Int KurExSet)), Cl KurExSet, Cl (Int KurExSet), Cl (Int (Cl KurExSet)) are_mutually_different by BORSUK_5:8; ::_thesis: verum end; theorem :: KURATO_1:55 card (Kurat7Set KurExSet) = 7 proof set A = KurExSet ; KurExSet , Int KurExSet, Cl KurExSet, Int (Cl KurExSet), Cl (Int KurExSet), Cl (Int (Cl KurExSet)), Int (Cl (Int KurExSet)) are_mutually_different by Th54, BORSUK_5:9; hence card (Kurat7Set KurExSet) = 7 by BORSUK_5:4; ::_thesis: verum end; begin registration cluster Kurat14ClPart KurExSet -> with_proper_subsets ; coherence Kurat14ClPart KurExSet is with_proper_subsets proof set A = KurExSet ; assume A1: the carrier of R^1 in Kurat14ClPart KurExSet ; :: according to SETFAM_1:def_12 ::_thesis: contradiction percases ( REAL = Cl KurExSet or REAL = Cl ((Cl KurExSet) `) or REAL = Cl ((Cl ((Cl KurExSet) `)) `) or REAL = Cl (KurExSet `) or REAL = Cl ((Cl (KurExSet `)) `) or REAL = Cl ((Cl ((Cl (KurExSet `)) `)) `) ) by A1, ENUMSET1:def_4, TOPMETR:17; suppose REAL = Cl KurExSet ; ::_thesis: contradiction hence contradiction by Th10, BORSUK_5:69; ::_thesis: verum end; suppose REAL = Cl ((Cl KurExSet) `) ; ::_thesis: contradiction hence contradiction by Th12, BORSUK_5:47; ::_thesis: verum end; suppose REAL = Cl ((Cl ((Cl KurExSet) `)) `) ; ::_thesis: contradiction hence contradiction by Th14, BORSUK_5:46; ::_thesis: verum end; suppose REAL = Cl (KurExSet `) ; ::_thesis: contradiction hence contradiction by Th17, BORSUK_5:70; ::_thesis: verum end; suppose REAL = Cl ((Cl (KurExSet `)) `) ; ::_thesis: contradiction hence contradiction by Th19, BORSUK_5:46; ::_thesis: verum end; suppose REAL = Cl ((Cl ((Cl (KurExSet `)) `)) `) ; ::_thesis: contradiction hence contradiction by Th21, BORSUK_5:47; ::_thesis: verum end; end; end; cluster Kurat14OpPart KurExSet -> with_proper_subsets ; coherence Kurat14OpPart KurExSet is with_proper_subsets proof set A = KurExSet ; assume A2: the carrier of R^1 in Kurat14OpPart KurExSet ; :: according to SETFAM_1:def_12 ::_thesis: contradiction percases ( REAL = (Cl KurExSet) ` or REAL = (Cl ((Cl KurExSet) `)) ` or REAL = (Cl ((Cl ((Cl KurExSet) `)) `)) ` or REAL = (Cl (KurExSet `)) ` or REAL = (Cl ((Cl (KurExSet `)) `)) ` or REAL = (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` ) by A2, ENUMSET1:def_4, TOPMETR:17; suppose REAL = (Cl KurExSet) ` ; ::_thesis: contradiction hence contradiction by Th10, BORSUK_5:72; ::_thesis: verum end; suppose REAL = (Cl ((Cl KurExSet) `)) ` ; ::_thesis: contradiction hence contradiction by Th12, BORSUK_5:72; ::_thesis: verum end; suppose REAL = (Cl ((Cl ((Cl KurExSet) `)) `)) ` ; ::_thesis: contradiction hence contradiction by Th14, BORSUK_5:72; ::_thesis: verum end; suppose REAL = (Cl (KurExSet `)) ` ; ::_thesis: contradiction hence contradiction by Th17, BORSUK_5:72; ::_thesis: verum end; suppose REAL = (Cl ((Cl (KurExSet `)) `)) ` ; ::_thesis: contradiction hence contradiction by Th19, BORSUK_5:72; ::_thesis: verum end; suppose REAL = (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` ; ::_thesis: contradiction hence contradiction by Th21, BORSUK_5:72; ::_thesis: verum end; end; end; end; registration cluster Kurat14Set KurExSet -> with_proper_subsets ; coherence Kurat14Set KurExSet is with_proper_subsets proof reconsider AA = {KurExSet,(KurExSet `)} as Subset-Family of R^1 by MEASURE1:2; AA is with_proper_subsets proof assume A1: the carrier of R^1 in AA ; :: according to SETFAM_1:def_12 ::_thesis: contradiction percases ( REAL = KurExSet or REAL = KurExSet ` ) by A1, TARSKI:def_2, TOPMETR:17; suppose REAL = KurExSet ; ::_thesis: contradiction then [#] R^1 = KurExSet by TOPMETR:17; hence contradiction ; ::_thesis: verum end; suppose REAL = KurExSet ` ; ::_thesis: contradiction then [#] R^1 = KurExSet ` by TOPMETR:17; hence contradiction by TOPS_1:3; ::_thesis: verum end; end; end; then A2: AA \/ (Kurat14ClPart KurExSet) is with_proper_subsets by SETFAM_1:48; Kurat14Set KurExSet = (AA \/ (Kurat14ClPart KurExSet)) \/ (Kurat14OpPart KurExSet) by Lm2; hence Kurat14Set KurExSet is with_proper_subsets by A2, SETFAM_1:48; ::_thesis: verum end; end; registration cluster Kurat14Set KurExSet -> with_non-empty_elements ; coherence Kurat14Set KurExSet is with_non-empty_elements proof reconsider E = {} R^1 as Subset of R^1 ; assume {} in Kurat14Set KurExSet ; :: according to SETFAM_1:def_8 ::_thesis: contradiction then E ` in Kurat14Set KurExSet by Th6; hence contradiction by SETFAM_1:def_12; ::_thesis: verum end; end; theorem Th56: :: KURATO_1:56 for A being with_non-empty_elements set for B being set st B c= A holds B is with_non-empty_elements proof let A be with_non-empty_elements set ; ::_thesis: for B being set st B c= A holds B is with_non-empty_elements let B be set ; ::_thesis: ( B c= A implies B is with_non-empty_elements ) assume A1: B c= A ; ::_thesis: B is with_non-empty_elements assume {} in B ; :: according to SETFAM_1:def_8 ::_thesis: contradiction hence contradiction by A1; ::_thesis: verum end; registration cluster Kurat14ClPart KurExSet -> with_non-empty_elements ; coherence Kurat14ClPart KurExSet is with_non-empty_elements proof Kurat14Set KurExSet = ({KurExSet,(KurExSet `)} \/ (Kurat14ClPart KurExSet)) \/ (Kurat14OpPart KurExSet) by Lm2; then A1: {KurExSet,(KurExSet `)} \/ (Kurat14ClPart KurExSet) c= Kurat14Set KurExSet by XBOOLE_1:7; Kurat14ClPart KurExSet c= {KurExSet,(KurExSet `)} \/ (Kurat14ClPart KurExSet) by XBOOLE_1:7; hence Kurat14ClPart KurExSet is with_non-empty_elements by A1, Th56, XBOOLE_1:1; ::_thesis: verum end; cluster Kurat14OpPart KurExSet -> with_non-empty_elements ; coherence Kurat14OpPart KurExSet is with_non-empty_elements proof Kurat14Set KurExSet = ({KurExSet,(KurExSet `)} \/ (Kurat14ClPart KurExSet)) \/ (Kurat14OpPart KurExSet) by Lm2; hence Kurat14OpPart KurExSet is with_non-empty_elements by Th56, XBOOLE_1:7; ::_thesis: verum end; end; registration cluster with_non-empty_elements with_proper_subsets for Element of bool (bool the carrier of R^1); existence ex b1 being Subset-Family of R^1 st ( b1 is with_proper_subsets & b1 is with_non-empty_elements ) proof take Kurat14Set KurExSet ; ::_thesis: ( Kurat14Set KurExSet is with_proper_subsets & Kurat14Set KurExSet is with_non-empty_elements ) thus ( Kurat14Set KurExSet is with_proper_subsets & Kurat14Set KurExSet is with_non-empty_elements ) ; ::_thesis: verum end; end; theorem Th57: :: KURATO_1:57 for F, G being with_non-empty_elements with_proper_subsets Subset-Family of R^1 st F is open & G is closed holds F misses G proof let F, G be with_non-empty_elements with_proper_subsets Subset-Family of R^1; ::_thesis: ( F is open & G is closed implies F misses G ) assume A1: ( F is open & G is closed ) ; ::_thesis: F misses G assume F meets G ; ::_thesis: contradiction then consider x being set such that A2: x in F and A3: x in G by XBOOLE_0:3; reconsider x = x as Subset of R^1 by A2; ( x is open & x is closed ) by A1, A2, A3, TOPS_2:def_1, TOPS_2:def_2; then ( x = {} or x = REAL ) by BORSUK_5:34; hence contradiction by A2, SETFAM_1:def_12, TOPMETR:17; ::_thesis: verum end; registration cluster Kurat14ClPart KurExSet -> closed ; coherence Kurat14ClPart KurExSet is closed proof let P be Subset of R^1; :: according to TOPS_2:def_2 ::_thesis: ( not P in Kurat14ClPart KurExSet or P is closed ) assume P in Kurat14ClPart KurExSet ; ::_thesis: P is closed hence P is closed by ENUMSET1:def_4; ::_thesis: verum end; cluster Kurat14OpPart KurExSet -> open ; coherence Kurat14OpPart KurExSet is open proof let P be Subset of R^1; :: according to TOPS_2:def_1 ::_thesis: ( not P in Kurat14OpPart KurExSet or P is open ) assume P in Kurat14OpPart KurExSet ; ::_thesis: P is open hence P is open by ENUMSET1:def_4; ::_thesis: verum end; end; theorem :: KURATO_1:58 Kurat14ClPart KurExSet misses Kurat14OpPart KurExSet by Th57; registration let T be non empty TopSpace; let A be Subset of T; cluster Kurat14ClPart A -> finite ; coherence Kurat14ClPart A is finite ; cluster Kurat14OpPart A -> finite ; coherence Kurat14OpPart A is finite ; end; theorem Th59: :: KURATO_1:59 card (Kurat14ClPart KurExSet) = 6 proof set A = KurExSet ; A1: Cl ((Cl ((Cl (KurExSet `)) `)) `) = ].-infty,4.] by Th20, BORSUK_5:51; 5 in {5} by TARSKI:def_1; then 5 in Cl (KurExSet `) by Th17, XBOOLE_0:def_3; then A2: ( Cl (Int KurExSet) = Cl ((Cl (KurExSet `)) `) & Cl (KurExSet `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `) ) by A1, TOPS_1:def_1, XXREAL_1:234; ( not 5 in Cl ((Cl ((Cl (KurExSet `)) `)) `) & 5 in [.2,+infty.[ ) by Th21, XXREAL_1:234, XXREAL_1:236; then A3: Cl KurExSet <> Cl ((Cl ((Cl (KurExSet `)) `)) `) by Th10, XBOOLE_0:def_3; ( not 5 in Cl ((Cl ((Cl (KurExSet `)) `)) `) & Cl ((Cl (KurExSet `)) `) = [.4,+infty.[ ) by Th18, Th21, BORSUK_5:55, XXREAL_1:234; then A4: Cl ((Cl (KurExSet `)) `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `) by XXREAL_1:236; 5 in Cl ((Cl ((Cl KurExSet) `)) `) by Th14, XXREAL_1:236; then A5: Cl ((Cl ((Cl KurExSet) `)) `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `) by Th21, XXREAL_1:234; ( not 6 in ].-infty,4.] & not 6 in {5} ) by TARSKI:def_1, XXREAL_1:234; then A6: not 6 in Cl (KurExSet `) by Th17, XBOOLE_0:def_3; Cl ((Cl ((Cl KurExSet) `)) `) = [.2,+infty.[ by Th13, BORSUK_5:49; then A7: Cl ((Cl ((Cl KurExSet) `)) `) <> Cl (KurExSet `) by A6, XXREAL_1:236; A8: ( 4 in Cl ((Cl ((Cl KurExSet) `)) `) & Cl (Int (Cl KurExSet)) = Cl ((Cl ((Cl KurExSet) `)) `) ) by Th14, TOPS_1:def_1, XXREAL_1:236; A9: not 4 in Cl ((Cl KurExSet) `) by Th12, XXREAL_1:234; then Cl ((Cl KurExSet) `) <> Cl ((Cl ((Cl (KurExSet `)) `)) `) by A1, XXREAL_1:234; then Cl KurExSet, Cl ((Cl KurExSet) `), Cl ((Cl ((Cl KurExSet) `)) `), Cl (KurExSet `), Cl ((Cl (KurExSet `)) `), Cl ((Cl ((Cl (KurExSet `)) `)) `) are_mutually_different by A9, A3, A7, A5, A8, A2, A4, Th29, Th31, ZFMISC_1:def_8; hence card (Kurat14ClPart KurExSet) = 6 by BORSUK_5:3; ::_thesis: verum end; theorem Th60: :: KURATO_1:60 card (Kurat14OpPart KurExSet) = 6 proof set A = KurExSet ; A1: ( not 5 in ].-infty,1.[ & not 5 in ].1,2.[ ) by XXREAL_1:4; ( (Cl KurExSet) ` = ].-infty,1.[ \/ ].1,2.[ & 5 in (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` ) by Th10, Th22, BORSUK_5:63, XXREAL_1:235; then A2: (Cl KurExSet) ` <> (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` by A1, XBOOLE_0:def_3; A3: (Cl ((Cl ((Cl KurExSet) `)) `)) ` = ].-infty,2.[ by Th14, TOPMETR:17, XXREAL_1:224, XXREAL_1:294; 6 in ].5,+infty.[ by XXREAL_1:235; then 6 in (Cl (KurExSet `)) ` by Th18, XBOOLE_0:def_3; then A4: (Cl ((Cl ((Cl KurExSet) `)) `)) ` <> (Cl (KurExSet `)) ` by A3, XXREAL_1:233; A5: 4 in (Cl ((Cl KurExSet) `)) ` by Th13, XXREAL_1:235; ( not 5 in ].4,5.[ & not 5 in ].5,+infty.[ ) by XXREAL_1:4; then A6: not 5 in (Cl (KurExSet `)) ` by Th18, XBOOLE_0:def_3; (Cl KurExSet) ` <> (Cl (Int (Cl KurExSet))) ` by Th29, BORSUK_5:71; then A7: (Cl KurExSet) ` <> (Cl ((Cl ((Cl KurExSet) `)) `)) ` by TOPS_1:def_1; A8: not 5 in (Cl ((Cl (KurExSet `)) `)) ` by Th20, XXREAL_1:233; (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` = ].4,+infty.[ by Th21, TOPMETR:17, XXREAL_1:224, XXREAL_1:288; then A9: (Cl ((Cl KurExSet) `)) ` <> (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` by A5, XXREAL_1:235; ( (Cl (Int (Cl KurExSet))) ` = (Cl ((Cl ((Cl KurExSet) `)) `)) ` & (Cl (Int KurExSet)) ` = (Cl ((Cl (KurExSet `)) `)) ` ) by TOPS_1:def_1; then A10: (Cl ((Cl ((Cl KurExSet) `)) `)) ` <> (Cl ((Cl (KurExSet `)) `)) ` by Th31, BORSUK_5:71; A11: ( not 5 in (Cl ((Cl ((Cl KurExSet) `)) `)) ` & 5 in (Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` ) by Th15, Th22, XXREAL_1:233, XXREAL_1:235; (Cl ((Cl KurExSet) `)) ` <> (Cl ((Cl ((Cl KurExSet) `)) `)) ` by A3, A5, XXREAL_1:233; then (Cl KurExSet) ` ,(Cl ((Cl KurExSet) `)) ` ,(Cl ((Cl ((Cl KurExSet) `)) `)) ` ,(Cl (KurExSet `)) ` ,(Cl ((Cl (KurExSet `)) `)) ` ,(Cl ((Cl ((Cl (KurExSet `)) `)) `)) ` are_mutually_different by A2, A7, A9, A4, A10, A6, A11, A8, ZFMISC_1:def_8; hence card (Kurat14OpPart KurExSet) = 6 by BORSUK_5:3; ::_thesis: verum end; theorem Th61: :: KURATO_1:61 {KurExSet,(KurExSet `)} misses Kurat14ClPart KurExSet proof set A = KurExSet ; assume {KurExSet,(KurExSet `)} meets Kurat14ClPart KurExSet ; ::_thesis: contradiction then consider x being set such that A1: x in {KurExSet,(KurExSet `)} and A2: x in Kurat14ClPart KurExSet by XBOOLE_0:3; reconsider x = x as Subset of R^1 by A2; ( x = KurExSet or x = KurExSet ` ) by A1, TARSKI:def_2; then A3: x ` = KurExSet by A2, TOPS_2:def_2; x is closed by A2, TOPS_2:def_2; hence contradiction by A3; ::_thesis: verum end; registration cluster KurExSet -> non empty ; coherence not KurExSet is empty ; end; theorem Th62: :: KURATO_1:62 KurExSet <> KurExSet ` proof assume KurExSet = KurExSet ` ; ::_thesis: contradiction then KurExSet meets KurExSet ` by XBOOLE_1:66; hence contradiction by XBOOLE_1:79; ::_thesis: verum end; theorem Th63: :: KURATO_1:63 {KurExSet,(KurExSet `)} misses Kurat14OpPart KurExSet proof set A = KurExSet ; assume {KurExSet,(KurExSet `)} meets Kurat14OpPart KurExSet ; ::_thesis: contradiction then consider x being set such that A1: x in {KurExSet,(KurExSet `)} and A2: x in Kurat14OpPart KurExSet by XBOOLE_0:3; reconsider x = x as Subset of R^1 by A2; ( x = KurExSet or x = KurExSet ` ) by A1, TARSKI:def_2; then A3: x ` = KurExSet by A2, TOPS_2:def_1; x is open by A2, TOPS_2:def_1; hence contradiction by A3; ::_thesis: verum end; theorem :: KURATO_1:64 card (Kurat14Set KurExSet) = 14 proof set A = KurExSet ; set B = {KurExSet,(KurExSet `)}; A1: {KurExSet,(KurExSet `)} misses (Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet) by Th61, Th63, XBOOLE_1:70; A2: card ((Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet)) = 6 + 6 by Th57, Th59, Th60, CARD_2:40 .= 12 ; card (Kurat14Set KurExSet) = card (({KurExSet,(KurExSet `)} \/ (Kurat14ClPart KurExSet)) \/ (Kurat14OpPart KurExSet)) by Lm2 .= card ({KurExSet,(KurExSet `)} \/ ((Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet))) by XBOOLE_1:4 .= (card {KurExSet,(KurExSet `)}) + (card ((Kurat14ClPart KurExSet) \/ (Kurat14OpPart KurExSet))) by A1, CARD_2:40 .= 2 + 12 by A2, Th62, CARD_2:57 .= 14 ; hence card (Kurat14Set KurExSet) = 14 ; ::_thesis: verum end; begin definition let T be TopStruct ; let A be Subset-Family of T; attrA is Cl-closed means :: KURATO_1:def 7 for P being Subset of T st P in A holds Cl P in A; attrA is Int-closed means :: KURATO_1:def 8 for P being Subset of T st P in A holds Int P in A; end; :: deftheorem defines Cl-closed KURATO_1:def_7_:_ for T being TopStruct for A being Subset-Family of T holds ( A is Cl-closed iff for P being Subset of T st P in A holds Cl P in A ); :: deftheorem defines Int-closed KURATO_1:def_8_:_ for T being TopStruct for A being Subset-Family of T holds ( A is Int-closed iff for P being Subset of T st P in A holds Int P in A ); registration let T be non empty TopSpace; let A be Subset of T; cluster Kurat14Set A -> non empty ; coherence not Kurat14Set A is empty ; cluster Kurat14Set A -> Cl-closed ; coherence Kurat14Set A is Cl-closed proof let P be Subset of T; :: according to KURATO_1:def_7 ::_thesis: ( P in Kurat14Set A implies Cl P in Kurat14Set A ) assume P in Kurat14Set A ; ::_thesis: Cl P in Kurat14Set A hence Cl P in Kurat14Set A by Th6; ::_thesis: verum end; cluster Kurat14Set A -> compl-closed ; coherence Kurat14Set A is compl-closed proof for P being Subset of T st P in Kurat14Set A holds P ` in Kurat14Set A by Th6; hence Kurat14Set A is compl-closed by PROB_1:def_1; ::_thesis: verum end; end; registration let T be non empty TopSpace; let A be Subset of T; cluster Kurat7Set A -> non empty ; coherence not Kurat7Set A is empty ; cluster Kurat7Set A -> Int-closed ; coherence Kurat7Set A is Int-closed proof let P be Subset of T; :: according to KURATO_1:def_8 ::_thesis: ( P in Kurat7Set A implies Int P in Kurat7Set A ) assume P in Kurat7Set A ; ::_thesis: Int P in Kurat7Set A hence Int P in Kurat7Set A by Th9; ::_thesis: verum end; cluster Kurat7Set A -> Cl-closed ; coherence Kurat7Set A is Cl-closed proof let P be Subset of T; :: according to KURATO_1:def_7 ::_thesis: ( P in Kurat7Set A implies Cl P in Kurat7Set A ) assume P in Kurat7Set A ; ::_thesis: Cl P in Kurat7Set A hence Cl P in Kurat7Set A by Th9; ::_thesis: verum end; end; registration let T be non empty TopSpace; cluster non empty Cl-closed Int-closed for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st ( b1 is Int-closed & b1 is Cl-closed & not b1 is empty ) proof take Kurat7Set ({} T) ; ::_thesis: ( Kurat7Set ({} T) is Int-closed & Kurat7Set ({} T) is Cl-closed & not Kurat7Set ({} T) is empty ) thus ( Kurat7Set ({} T) is Int-closed & Kurat7Set ({} T) is Cl-closed & not Kurat7Set ({} T) is empty ) ; ::_thesis: verum end; cluster non empty compl-closed Cl-closed for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st ( b1 is compl-closed & b1 is Cl-closed & not b1 is empty ) proof take Kurat14Set ({} T) ; ::_thesis: ( Kurat14Set ({} T) is compl-closed & Kurat14Set ({} T) is Cl-closed & not Kurat14Set ({} T) is empty ) thus ( Kurat14Set ({} T) is compl-closed & Kurat14Set ({} T) is Cl-closed & not Kurat14Set ({} T) is empty ) ; ::_thesis: verum end; end;