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 that
A1: S is closed and
A2: T c= S ; :: thesis: Cl T c= S
Cl S = S by A1, PRE_TOPC:22;
hence Cl T c= S by A2, PRE_TOPC:19; :: thesis: verum