X c= REAL n ;
then X c= [#] (REAL n) by SUBSET_1:def 4;
then [#] (REAL n) in { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } ;
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