let GX be TopStruct ; :: thesis: for S, T being Subset of GX st S is closed & T c= S holds
Cl T c= S
let S, T be Subset of GX; :: thesis: ( S is closed & T c= S implies Cl T c= S )
assume A1: ( S is closed & T c= S ) ; :: thesis: Cl T c= S
then Cl S = S by PRE_TOPC:52;
hence Cl T c= S by A1, PRE_TOPC:49; :: thesis: verum