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 )

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

A2:
( X meets Z implies X meets Y \/ Z )
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;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

proof

( X meets Y implies X meets Y \/ Z )
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;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

proof

hence
( ( X meets Y or X meets Z ) implies X meets Y \/ Z )
by A2; :: thesis: verum
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;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