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