set X = F_{1}();

consider c being Function such that

A5: ( dom c = bool F_{1}() & ( for a being set st a in bool F_{1}() holds

c . a = F_{2}(a) ) )
from FUNCT_1:sch 5();

_{1}()),(bool F_{1}()) by A5, FUNCT_2:3;

A8: for A being Subset of F_{1}() holds c . A c= A
_{1}() holds c . (A /\ B) = (c . A) /\ (c . B)
_{1}() holds c . (c . A) = c . A
_{1}() = F_{1}()
by A1, A5;

then reconsider T = TopStruct(# F_{1}(),(rng c) #) as strict TopSpace by A12, A8, A9, Th9;

take T ; :: thesis: ( the carrier of T = F_{1}() & ( for A being Subset of T holds Int A = F_{2}(A) ) )

thus the carrier of T = F_{1}()
; :: thesis: for A being Subset of T holds Int A = F_{2}(A)

let A be Subset of T; :: thesis: Int A = F_{2}(A)

thus Int A = c . A by A14, A8, A9, A12, Th9

.= F_{2}(A)
by A5
; :: thesis: verum

consider c being Function such that

A5: ( dom c = bool F

c . a = F

now :: thesis: for a being object st a in bool F_{1}() holds

c . a in bool F_{1}()

then reconsider c = c as Function of (bool Fc . a in bool F

let a be object ; :: thesis: ( a in bool F_{1}() implies c . a in bool F_{1}() )

assume A6: a in bool F_{1}()
; :: thesis: c . a in bool F_{1}()

reconsider aa = a as set by TARSKI:1;

A7: F_{2}(a) c= aa
by A2, A6;

c . a = F_{2}(a)
by A6, A5;

then c . a c= F_{1}()
by A7, A6, XBOOLE_1:1;

hence c . a in bool F_{1}()
; :: thesis: verum

end;assume A6: a in bool F

reconsider aa = a as set by TARSKI:1;

A7: F

c . a = F

then c . a c= F

hence c . a in bool F

A8: for A being Subset of F

proof

A9:
for A, B being Subset of F
let A be Subset of F_{1}(); :: thesis: c . A c= A

c . A = F_{2}(A)
by A5;

hence c . A c= A by A2; :: thesis: verum

end;c . A = F

hence c . A c= A by A2; :: thesis: verum

proof

A12:
for A being Subset of F
let A, B be Subset of F_{1}(); :: thesis: c . (A /\ B) = (c . A) /\ (c . B)

A10: c . B = F_{2}(B)
by A5;

A11: F_{2}((A /\ B)) = c . (A /\ B)
by A5;

c . A = F_{2}(A)
by A5;

hence c . (A /\ B) = (c . A) /\ (c . B) by A10, A11, A3; :: thesis: verum

end;A10: c . B = F

A11: F

c . A = F

hence c . (A /\ B) = (c . A) /\ (c . B) by A10, A11, A3; :: thesis: verum

proof

A14:
c . F
let A be Subset of F_{1}(); :: thesis: c . (c . A) = c . A

A13: F_{2}((c . A)) = c . (c . A)
by A5;

c . A = F_{2}(A)
by A5;

hence c . (c . A) = c . A by A13, A4; :: thesis: verum

end;A13: F

c . A = F

hence c . (c . A) = c . A by A13, A4; :: thesis: verum

then reconsider T = TopStruct(# F

take T ; :: thesis: ( the carrier of T = F

thus the carrier of T = F

let A be Subset of T; :: thesis: Int A = F

thus Int A = c . A by A14, A8, A9, A12, Th9

.= F