let Y be set ; :: thesis: for A being non empty set st A c= Y holds
A meets Y
let A be non empty set ; :: thesis: ( A c= Y implies A meets Y )
assume A c= Y ; :: thesis: A meets Y
hence A /\ Y <> {} by Th28; :: according to XBOOLE_0:def 7 :: thesis: verum