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