let T be with_properly_defined_topology 1TopStruct ; :: thesis: ( T is with_preclosure implies T is TopSpace-like )
set f = the FirstOp of T;
assume T is with_preclosure ; :: thesis: T is TopSpace-like
then T1: the FirstOp of T is preclosure ;
the FirstOp of T is empty-preserving by T1;
then {} T is op-closed ;
then XX: ({} T) ` in the topology of T by PDT;
s: ([#] T) ` = (({} T) `) ` ;
X2: the FirstOp of T is extensive by T1;
[#] T = the FirstOp of T . ([#] T) by X2;
then aa: ({} T) ` is op-closed ;
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;

per cases ( a = {} or a <> {} ) ;

suppose a = {} ; :: thesis: union a in the topology of T

hence union a in the topology of T by aa, ZFMISC_1:2, s, PDT; :: thesis: verum

end;

suppose xx: a <> {} ; :: thesis: union a in the topology of T

then f2: ([#] the carrier of T) \ ua = meet (COMPLEMENT a) by SETFAM_1:33;
f3: the FirstOp of T is extensive by T1;
the FirstOp of T . (meet (COMPLEMENT a)) c= meet (COMPLEMENT a)

proof

for bb being set st bb in COMPLEMENT a holds
the FirstOp of T . (meet (COMPLEMENT a)) c= bb

proof

let bb be set ; :: thesis: ( bb in COMPLEMENT a implies the FirstOp of T . (meet (COMPLEMENT a)) c= bb )
assume FG: bb in COMPLEMENT a ; :: thesis: the FirstOp of T . (meet (COMPLEMENT a)) c= bb
reconsider b1 = bb as Subset of T by FG;
fh: the FirstOp of T is c=-monotone by T1;
b1 ` in a by FG, SETFAM_1:def 7;
then consider F being Subset of T such that
J1: ( F ` = b1 ` & F is op-closed ) by PDT, J0;
(F `) ` = (b1 `) ` by J1;
hence the FirstOp of T . (meet (COMPLEMENT a)) c= bb by fh, FG, SETFAM_1:3, J1; :: thesis: verum

end;

hence the FirstOp of T . (meet (COMPLEMENT a)) c= meet (COMPLEMENT a) by SETFAM_1:5, xx, SETFAM_1:32; :: thesis: verum

end;

then meet (COMPLEMENT a) = the FirstOp of T . (meet (COMPLEMENT a)) by f3;
then ua ` is op-closed by f2;
then (ua `) ` in the topology of T by PDT;
hence union a in the topology of T ; :: thesis: verum

end;

end;

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-closed ) by PDT;
consider B being Subset of T such that
Y2: ( B ` = b & B is op-closed ) by PDT, Y0;
zz: ( the FirstOp of T is extensive & the FirstOp of T is \/-preserving & the FirstOp of T is empty-preserving ) by T1;
ZZ: A \/ B is op-closed by zz, Y1, Y2;
a /\ b = (A \/ B) ` by XBOOLE_1:53, Y1, Y2;
hence a /\ b in the topology of T by PDT, ZZ; :: thesis: verum

end;

hence T is TopSpace-like by XX, A2, PRE_TOPC:def 1; :: thesis: verum