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 object such that
A1: ( x in X & x in Y \/ Z ) by XBOOLE_0:3;
( ( x in X & x in Y ) or ( x in X & x in Z ) ) by A1, XBOOLE_0:def 3;
hence ( X meets Y or X meets Z ) by XBOOLE_0:3; :: thesis: verum
end;
A2: ( X meets Z implies X meets Y \/ Z )
proof
assume X meets Z ; :: thesis: X meets Y \/ Z
then consider x being object such that
A3: x in X and
A4: x in Z by XBOOLE_0:3;
x in Y \/ Z by A4, XBOOLE_0:def 3;
hence X meets Y \/ Z by A3, XBOOLE_0:3; :: thesis: verum
end;
( X meets Y implies X meets Y \/ Z )
proof
assume X meets Y ; :: thesis: X meets Y \/ Z
then consider x being object such that
A5: x in X and
A6: x in Y by XBOOLE_0:3;
x in Y \/ Z by A6, XBOOLE_0:def 3;
hence X meets Y \/ Z by A5, XBOOLE_0:3; :: thesis: verum
end;
hence ( ( X meets Y or X meets Z ) implies X meets Y \/ Z ) by A2; :: thesis: verum