let T be non empty TopSpace; :: thesis:
let A, Q be Subset of T; :: thesis:
assume A1: Q in Kurat7Set A ; :: thesis:
( Int Q in Kurat7Set A & Cl Q in Kurat7Set A )

proof

per cases by A1, ENUMSET1:def 5;

suppose Q = A ; :: thesis:

hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def 5; :: thesis:

end;

suppose Q = Int A ; :: thesis:

hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def 5; :: thesis:

end;

suppose Q = Cl A ; :: thesis:

hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def 5; :: thesis:

end;

suppose Q = Int (Cl A) ; :: thesis:

hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def 5; :: thesis:

end;

suppose Q = Cl (Int A) ; :: thesis:

hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) by ENUMSET1:def 5; :: thesis:

end;

suppose A2: Q = Cl (Int (Cl A)) ; :: thesis:

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:

end;

suppose A3: Q = Int (Cl (Int A)) ; :: thesis:

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:

end;

end;

end;

hence ( Int Q in Kurat7Set A & Cl Q in Kurat7Set A ) ; :: thesis: