let X be RealNormSpace; :: thesis: for A being Subset of X ex F being Subset-Family of X st
( ( for C being Subset of X holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
let A be Subset of X; :: thesis: ex F being Subset-Family of X st
( ( for C being Subset of X holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
reconsider B = A as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
consider G being Subset-Family of (LinearTopSpaceNorm X) such that
A1: ( ( for C being Subset of (LinearTopSpaceNorm X) holds
( C in G iff ( C is closed & B c= C ) ) ) & Cl B = meet G ) by PRE_TOPC:16;
reconsider F = G as Subset-Family of X by NORMSP_2:def 4;
for C being Subset of X holds
( C in F iff ( C is closed & A c= C ) )
proof
let C be Subset of X; :: thesis: ( C in F iff ( C is closed & A c= C ) )
reconsider D = C as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
( D in G iff ( D is closed & B c= D ) ) by A1;
hence ( C in F iff ( C is closed & A c= C ) ) by NORMSP_2:32; :: thesis: verum
end;
hence ex F being Subset-Family of X st
( ( for C being Subset of X holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F ) by A1, EQCL1; :: thesis: verum