let T be 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)))}
let A be Subset of T; 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)))}
; verum