let GX be TopStruct ; :: thesis: Cl ([#] GX) = [#] GX
thus Cl ([#] GX) c= [#] GX ; :: according to XBOOLE_0:def 10 :: thesis: [#] GX c= Cl ([#] GX)
thus [#] GX c= Cl ([#] GX) by PRE_TOPC:18; :: thesis: verum