let T be non empty with_equivalence naturally_generated TopRelStr ; :: thesis: for A being Subset of T holds Kurat14Set A = {A,(UAp A),((UAp A) `),(A `),((LAp A) `),(LAp A)}
let A be Subset of T; :: thesis: Kurat14Set A = {A,(UAp A),((UAp A) `),(A `),((LAp A) `),(LAp A)}

Z1: now :: thesis: for A being Subset of T holds Kurat14Part A = {A,(A -),((A -) `)}

let A be Subset of T; :: thesis: Kurat14Part A = {A,(A -),((A -) `)}
(((A -) `) -) ` = ((LAp (A -)) `) ` by ROUGHS_1:29;
then (((A -) `) -) ` = UAp (UAp A) by ROUGHS_1:36
.= UAp A ;
hence Kurat14Part A = {A,(A -),((A -) `),((A -) `)} \/ {(A -),(A -),((A -) `)} by ENUMSET1:19
.= {A,(A -),((A -) `),((A -) `)} \/ {(A -),((A -) `)} by ENUMSET1:30
.= ({A,(A -)} \/ {((A -) `),((A -) `)}) \/ {(A -),((A -) `)} by ENUMSET1:5
.= ({A,(A -)} \/ {((A -) `)}) \/ {(A -),((A -) `)} by ENUMSET1:29
.= {A,(A -)} \/ ({((A -) `)} \/ {(A -),((A -) `)}) by XBOOLE_1:4
.= {A,(A -)} \/ {((A -) `),(A -),((A -) `)} by ENUMSET1:2
.= {A,(A -)} \/ {(A -),((A -) `),((A -) `)} by ENUMSET1:58
.= {A,(A -)} \/ ({(A -)} \/ {((A -) `),((A -) `)}) by ENUMSET1:2
.= {A,(A -)} \/ ({(A -)} \/ {((A -) `)}) by ENUMSET1:29
.= ({A,(A -)} \/ {(A -)}) \/ {((A -) `)} by XBOOLE_1:4
.= {A,(A -),(A -)} \/ {((A -) `)} by ENUMSET1:3
.= {(A -),(A -),A} \/ {((A -) `)} by ENUMSET1:59
.= {A,(A -)} \/ {((A -) `)} by ENUMSET1:30
.= {A,(A -),((A -) `)} by ENUMSET1:3 ;
:: thesis: verum

end;

then Z2: Kurat14Part (A `) = {(A `),((A `) -),(((A `) -) `)} ;
z3: Kurat14Part A = {A,(A -),((A -) `)} by Z1;
((A `) -) ` = ((LAp A) `) ` by ROUGHS_1:29;
hence Kurat14Set A = {A,(UAp A),((UAp A) `),(A `),((LAp A) `),(LAp A)} by ENUMSET1:13, z3, Z2; :: thesis: verum