let X, Y, Z be set ; :: thesis: ( ( X meets Y or X meets Z ) iff X meets Y \/ Z )
thus ( not X meets Y \/ Z or X meets Y or X meets Z ) :: thesis: ( ( X meets Y or X meets Z ) implies X meets Y \/ Z )

proof

assume X meets Y \/ Z ; :: thesis: ( X meets Y or X meets Z )
then consider x being set such that
A1: x in X and
A2: x in Y \/ Z by XBOOLE_0:3;
( ( x in X & x in Y ) or ( x in X & x in Z ) ) by A1, A2, XBOOLE_0:def 3;
hence ( X meets Y or X meets Z ) by XBOOLE_0:3; :: thesis: verum

end;

A3: ( X meets Y implies X meets Y \/ Z )

proof

assume X meets Y ; :: thesis: X meets Y \/ Z
then consider x being set such that
A4: ( x in X & x in Y ) by XBOOLE_0:3;
( x in X & x in Y \/ Z ) by A4, XBOOLE_0:def 3;
hence X meets Y \/ Z by XBOOLE_0:3; :: thesis: verum

end;

( X meets Z implies X meets Y \/ Z )

proof

assume X meets Z ; :: thesis: X meets Y \/ Z
then consider x being set such that
A5: ( x in X & x in Z ) by XBOOLE_0:3;
( x in X & x in Y \/ Z ) by A5, XBOOLE_0:def 3;
hence X meets Y \/ Z by XBOOLE_0:3; :: thesis: verum

end;

hence ( ( X meets Y or X meets Z ) implies X meets Y \/ Z ) by A3; :: thesis: verum