let T be non empty with_equivalence naturally_generated TopRelStr ; 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; Kurat14Set A = {A,(UAp A),((UAp A) `),(A `),((LAp A) `),(LAp A)}
Z1:
now for A being Subset of T holds Kurat14Part A = {A,(A -),((A -) `)}let A be
Subset of
T;
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
;
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; verum