set X = F₁();
consider c being Function such that
A5: ( dom c = bool F₁() & ( for a being set st a in bool F₁() holds
c . a = F₂(a) ) ) from FUNCT_1:sch 3();

now

let a be set ; :: thesis: ( a in bool F₁() implies c . a in bool F₁() )
assume a in bool F₁() ; :: thesis: c . a in bool F₁()
then ( c . a = F₂(a) & F₂(a) c= F₁() ) by A2, A5;
hence c . a in bool F₁() ; :: thesis: verum

end;

then reconsider c = c as Function of (bool F₁()),(bool F₁()) by A5, FUNCT_2:5;
{} c= F₁() by XBOOLE_1:2;
then A6: c . {} = {} by A1, A5;
A7: for A being Subset of F₁() holds A c= c . A

proof

let A be Subset of F₁(); :: thesis: A c= c . A
c . A = F₂(A) by A5;
hence A c= c . A by A2; :: thesis: verum

end;

A8: for A, B being Subset of F₁() holds c . (A \/ B) = (c . A) \/ (c . B)

proof

let A, B be Subset of F₁(); :: thesis: c . (A \/ B) = (c . A) \/ (c . B)
( c . A = F₂(A) & c . B = F₂(B) & F₂((A \/ B)) = c . (A \/ B) ) by A5;
hence c . (A \/ B) = (c . A) \/ (c . B) by A3; :: thesis: verum

end;

A9: for A being Subset of F₁() holds c . (c . A) = c . A

proof

let A be Subset of F₁(); :: thesis: c . (c . A) = c . A
( c . A = F₂(A) & F₂((c . A)) = c . (c . A) ) by A5;
hence c . (c . A) = c . A by A4; :: thesis: verum

end;

then reconsider T = TopStruct(# F₁(),(COMPLEMENT (rng c)) #) as strict TopSpace by A6, A7, A8, Th7;
take T ; :: thesis: ( the carrier of T = F₁() & ( for A being Subset of T holds Cl A = F₂(A) ) )
thus the carrier of T = F₁() ; :: thesis: for A being Subset of T holds Cl A = F₂(A)
let A be Subset of T; :: thesis: Cl A = F₂(A)
thus Cl A = c . A by A6, A7, A8, A9, Th7
.= F₂(A) by A5 ; :: thesis: verum