let Y, Z be set ; :: thesis: for A being non empty set st A c= Y & A c= Z holds
Y meets Z
let A be non empty set ; :: thesis: ( A c= Y & A c= Z implies Y meets Z )
consider x being object such that
A1: x in A by XBOOLE_0:def 1;
assume ( A c= Y & A c= Z ) ; :: thesis: Y meets Z
then ( x in Y & x in Z ) by A1;
hence Y meets Z by XBOOLE_0:3; :: thesis: verum