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