set IT = TopRelStr(# C,I,f #);
A1: C in the topology of TopRelStr(# C,I,f #) by TLDef;
( f is V97() & f is union-closed ) by TLDef;
hence TopRelStr(# C,I,f #) is TopSpace-like by PRE_TOPC:def 1, A1; :: thesis: verum