l .: X c= [#] F ;
hence l .: X is Subset of F ; :: thesis: verum