let TX be non empty TopSpace; :: thesis: for P being Subset of TX
for A being Subset of (TX | P)
for B being Subset of TX st B is closed & A = B /\ P holds
A is closed
let P be Subset of TX; :: thesis: for A being Subset of (TX | P)
for B being Subset of TX st B is closed & A = B /\ P holds
A is closed
let A be Subset of (TX | P); :: thesis: for B being Subset of TX st B is closed & A = B /\ P holds
A is closed
let B be Subset of TX; :: thesis: ( B is closed & A = B /\ P implies A is closed )
assume that
A1: B is closed and
A2: A = B /\ P ; :: thesis: A is closed
[#] (TX | P) = P by PRE_TOPC:def 5;
hence A is closed by A1, A2, PRE_TOPC:13; :: thesis: verum