let R be non empty with_equivalence TopRelStr ; :: thesis: ( R is naturally_generated implies R is TopSpace-like )
set f = LAp R;
set F = GenTop (LAp R);
assume tt: R is naturally_generated ; :: thesis: R is TopSpace-like
a1: GenTop (LAp R) is topology-like by ImportTop;
GenTop (LAp R) is topology-like by ImportTop;
then ( GenTop (LAp R) is V97() & GenTop (LAp R) is union-closed ) ;
hence R is TopSpace-like by PRE_TOPC:def 1, a1, tt; :: thesis: verum