X c= REAL n ;
then X c= [#] (REAL n) by SUBSET_1:def 3;
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:7; :: thesis: verum