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

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