let T be with_properly_defined_Topology 2TopStruct ; :: thesis: ( T is with_preinterior implies T is TopSpace-like )
set f = the SecondOp of T;
assume T is with_preinterior ; :: thesis: T is TopSpace-like
then T1: the SecondOp of T is preinterior ;
the SecondOp of T is universe-preserving by T1;
then xx: [#] T is op-open ;
A1: the carrier of T in the topology of T by PDTo, xx;
A2: for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T
proof
let a be Subset-Family of T; :: thesis: ( a c= the topology of T implies union a in the topology of T )
assume J0: a c= the topology of T ; :: thesis: union a in the topology of T
reconsider ua = union a as Subset of T ;
set b = COMPLEMENT a;
f3: the SecondOp of T is intensive by T1;
union a c= the SecondOp of T . (union a)
proof
for bb being set st bb in a holds
bb c= the SecondOp of T . (union a)
proof
let bb be set ; :: thesis: ( bb in a implies bb c= the SecondOp of T . (union a) )
assume FG: bb in a ; :: thesis: bb c= the SecondOp of T . (union a)
reconsider b1 = bb as Subset of T by FG;
fh: the SecondOp of T is c=-monotone by T1;
ex F being Subset of T st
( F = b1 & F is op-open ) by PDTo, J0, FG;
hence bb c= the SecondOp of T . (union a) by fh, FG, ZFMISC_1:74; :: thesis: verum
end;
hence union a c= the SecondOp of T . (union a) by ZFMISC_1:76; :: thesis: verum
end;
then union a = the SecondOp of T . (union a) by f3;
then ua is op-open ;
hence union a in the topology of T by PDTo; :: thesis: verum
end;
for a, b being Subset of T st a in the topology of T & b in the topology of T holds
a /\ b in the topology of T
proof
let a, b be Subset of T; :: thesis: ( a in the topology of T & b in the topology of T implies a /\ b in the topology of T )
assume Y0: ( a in the topology of T & b in the topology of T ) ; :: thesis: a /\ b in the topology of T
then consider A being Subset of T such that
Y1: ( A = a & A is op-open ) by PDTo;
consider B being Subset of T such that
Y2: ( B = b & B is op-open ) by PDTo, Y0;
zz: ( the SecondOp of T is intensive & the SecondOp of T is /\-preserving & the SecondOp of T is universe-preserving ) by T1;
A /\ B is op-open by zz, Y1, Y2;
hence a /\ b in the topology of T by PDTo, Y1, Y2; :: thesis: verum
end;
hence T is TopSpace-like by A1, A2, PRE_TOPC:def 1; :: thesis: verum