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= a & a c= F₁() ) by A2, A5;
then c . a c= F₁() by XBOOLE_1:1;
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;
F₁() c= F₁() ;
then A6: c . F₁() = F₁() by A1, A5;
A7: for A being Subset of F₁() holds c . A c= A

proof

let A be Subset of F₁(); :: thesis: c . A c= A
c . A = F₂(A) by A5;
hence c . A 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₁(),(rng c) #) as strict TopSpace by A6, A7, A8, Th9;
take T ; :: thesis: ( the carrier of T = F₁() & ( for A being Subset of T holds Int A = F₂(A) ) )
thus the carrier of T = F₁() ; :: thesis: for A being Subset of T holds Int A = F₂(A)
let A be Subset of T; :: thesis: Int A = F₂(A)
thus Int A = c . A by A6, A7, A8, A9, Th9
.= F₂(A) by A5 ; :: thesis: verum