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 )
assume A1: ( A c= Y & A c= Z ) ; :: thesis: Y meets Z
consider x being set such that
A2: x in A by XBOOLE_0:def 1;
( x in Y & x in Z ) by A1, A2, TARSKI:def 3;
hence Y meets Z by XBOOLE_0:3; :: thesis: verum