let X be set ; :: thesis:
let f be Function of (bool X),(bool X); :: thesis:
assume AA: f is preinterior ; :: thesis:
set F = GenTop f;
a1: ex S being Subset of X st
( S = X & S is f -closed )

proof

take S = [#] X; :: thesis:
f is universe-preserving by AA;
hence ( S = X & S is f -closed ) ; :: thesis:

end;

a0: ex S being Subset of X st
( S = {} & S is f -closed )

proof

take S = {} X; :: thesis:
f is intensive by AA;
then f . S c= S ;
hence ( S = {} & S is f -closed ) ; :: thesis:

end;

A2: GenTop f is V97()

proof

let a, b be Subset of X; :: according to ROUGHS_4:def 2 :: thesis:
assume Y0: ( a in GenTop f & b in GenTop f ) ; :: thesis:
then consider A being Subset of X such that
Y1: ( A = a & A is f -closed ) by GTDef;
consider B being Subset of X such that
Y2: ( B = b & B is f -closed ) by GTDef, Y0;
( f is intensive & f is /\-preserving & f is universe-preserving ) by AA;
then A /\ B is f -closed by Y1, Y2;
hence a /\ b in GenTop f by GTDef, Y1, Y2; :: thesis:

end;

for a being Subset-Family of X st a c= GenTop f holds
union a in GenTop f

proof

let a be Subset-Family of X; :: thesis:
assume J0: a c= GenTop f ; :: thesis:
reconsider ua = union a as Subset of X ;
set b = COMPLEMENT a;
f3: f is intensive by AA;
union a c= f . (union a)

proof

for bb being set st bb in a holds
bb c= f . (union a)

proof

let bb be set ; :: thesis:
assume FG: bb in a ; :: thesis:
reconsider b1 = bb as Subset of X by FG;
fh: f is c=-monotone by AA;
consider F being Subset of X such that
J1: ( F = b1 & F is f -closed ) by GTDef, FG, J0;
thus bb c= f . (union a) by fh, J1, FG, ZFMISC_1:74; :: thesis:

end;

hence union a c= f . (union a) by ZFMISC_1:76; :: thesis:

end;

then union a = f . (union a) by f3;
then ua is f -closed ;
hence union a in GenTop f by GTDef; :: thesis:

end;

then GenTop f is union-closed ;
hence GenTop f is topology-like by a0, a1, A2, GTDef; :: thesis: