let x, y, A, B be set ; :: thesis: ( x in A \/ B & y in A \/ B & not ( x in A \ B & y in A \ B ) & not ( x in B & y in B ) & not ( x in A \ B & y in B ) implies ( x in B & y in A \ B ) )
assume A1: ( x in A \/ B & y in A \/ B ) ; :: thesis: ( ( x in A \ B & y in A \ B ) or ( x in B & y in B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) )
A \/ B = (A \ B) \/ B by XBOOLE_1:39;
hence ( ( x in A \ B & y in A \ B ) or ( x in B & y in B ) or ( x in A \ B & y in B ) or ( x in B & y in A \ B ) ) by A1, XBOOLE_0:def 3; :: thesis: verum