let TX be non empty TopSpace; :: thesis: for P being Subset of
for A being Subset of
for B being Subset of st B is closed & A = B /\ P holds
A is closed
let P be Subset of ; :: thesis: for A being Subset of
for B being Subset of st B is closed & A = B /\ P holds
A is closed
let A be Subset of ; :: thesis: for B being Subset of st B is closed & A = B /\ P holds
A is closed
let B be Subset of ; :: 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 10;
hence A is closed by A1, A2, PRE_TOPC:43; :: thesis: verum