X c= REAL n ;
then A1: X c= [#] (REAL n) by SUBSET_1:def 4;
[#] (REAL n) in { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } by A1;
hence meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } is Subset of (REAL n) by SETFAM_1:8; :: thesis: verum