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

per cases ( 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;

suppose A2: 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;

suppose A3: 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