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