let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds Kurat7Set A = {A,(Cl A),(Int A)}
let A be Subset of T; :: thesis: Kurat7Set A = {A,(Cl A),(Int A)}
A1: Cl (Int (Cl A)) = Cl A by ROUGHS_1:30;
Kurat7Set A = ({A} \/ {(Int A),(Int (Cl A)),(Int (Cl (Int A)))}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))} by KURATO_1:8
.= ({A} \/ {(Int A),(Int (Cl A)),(Int A)}) \/ {(Cl A),(Cl (Int A)),(Cl (Int (Cl A)))} by ROUGHS_1:31
.= ({A} \/ {(Int A),(Int A),(Int (Cl A))}) \/ {(Cl A),(Cl (Int A)),(Cl A)} by ENUMSET1:57, A1
.= ({A} \/ {(Int A),(Int (Cl A))}) \/ {(Cl A),(Cl (Int A)),(Cl A)} by ENUMSET1:30
.= ({A} \/ {(Int A),(Int (Cl A))}) \/ {(Cl A),(Cl A),(Cl (Int A))} by ENUMSET1:57
.= ({A} \/ {(Int A),(Int (Cl A))}) \/ {(Cl A),(Cl (Int A))} by ENUMSET1:30
.= ({A} \/ {(Int A),(Cl (Cl A))}) \/ {(Cl A),(Cl (Int A))} by ROUGHS_1:36
.= ({A} \/ {(Int A),(Cl A)}) \/ {(Cl A),(Int (Int A))} by ROUGHS_1:34
.= {A} \/ ({(Cl A),(Int A)} \/ {(Cl A),(Int A)}) by XBOOLE_1:4
.= {A,(Cl A),(Int A)} by ENUMSET1:2 ;
hence Kurat7Set A = {A,(Cl A),(Int A)} ; :: thesis: verum