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 ) )

( ( 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

( ( 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

hence
ex F being Subset-Family of X st
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;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

( ( 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