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

proof

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

end;

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

proof

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

end;

A2: GenTop f is cap-closed

proof

let a, b be Subset of X; :: according to ROUGHS_4:def 2 :: thesis: ( a in GenTop f & b in GenTop f implies a /\ b in GenTop f )
assume Y0: ( a in GenTop f & b in GenTop f ) ; :: thesis: a /\ b in GenTop f
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: verum

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: ( a c= GenTop f implies union a in GenTop f )
assume J0: a c= GenTop f ; :: thesis: union a in GenTop f
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: ( bb in a implies bb c= f . (union a) )
assume FG: bb in a ; :: thesis: bb c= f . (union a)
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: verum

end;

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

end;

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

end;

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