let GX be TopSpace; :: thesis: for A, B being Subset of GX

for AA being Subset of (GX | B) st A = AA holds

GX | A = (GX | B) | AA

let A, B be Subset of GX; :: thesis: for AA being Subset of (GX | B) st A = AA holds

GX | A = (GX | B) | AA

let AA be Subset of (GX | B); :: thesis: ( A = AA implies GX | A = (GX | B) | AA )

assume A1: A = AA ; :: thesis: GX | A = (GX | B) | AA

the carrier of (GX | A) = [#] (GX | A)

.= A by PRE_TOPC:def 5 ;

then reconsider GY = GX | A as strict SubSpace of GX | B by A1, TSEP_1:4;

[#] GY = AA by A1, PRE_TOPC:def 5;

hence GX | A = (GX | B) | AA by PRE_TOPC:def 5; :: thesis: verum

for AA being Subset of (GX | B) st A = AA holds

GX | A = (GX | B) | AA

let A, B be Subset of GX; :: thesis: for AA being Subset of (GX | B) st A = AA holds

GX | A = (GX | B) | AA

let AA be Subset of (GX | B); :: thesis: ( A = AA implies GX | A = (GX | B) | AA )

assume A1: A = AA ; :: thesis: GX | A = (GX | B) | AA

the carrier of (GX | A) = [#] (GX | A)

.= A by PRE_TOPC:def 5 ;

then reconsider GY = GX | A as strict SubSpace of GX | B by A1, TSEP_1:4;

[#] GY = AA by A1, PRE_TOPC:def 5;

hence GX | A = (GX | B) | AA by PRE_TOPC:def 5; :: thesis: verum