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

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