let a be Subset-Family of T; :: thesis:
assume J0: a c= the topology of T ; :: thesis:
reconsider ua = union a as Subset of T ;
set b = COMPLEMENT a;

end;

let bb be set ; :: thesis:
assume FG: bb in COMPLEMENT a ; :: thesis:
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:

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

let a, b be Subset of T; :: thesis:
assume Y0: ( a in the topology of T & b in the topology of T ) ; :: thesis:
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:

end;