let X, Y be set ; :: thesis: ( [:X,Y:] = {} iff ( X = {} or Y = {} ) )
thus ( not [:X,Y:] = {} or X = {} or Y = {} ) :: thesis: ( ( X = {} or Y = {} ) implies [:X,Y:] = {} )

proof

assume A1: [:X,Y:] = {} ; :: thesis: ( X = {} or Y = {} )
assume X <> {} ; :: thesis: Y = {}
then consider x being set such that
A2: x in X by XBOOLE_0:7;
assume Y <> {} ; :: thesis: contradiction
then consider y being set such that
A3: y in Y by XBOOLE_0:7;
[x,y] in [:X,Y:] by A2, A3, Def2;
hence contradiction by A1; :: thesis: verum

end;

assume A4: ( ( X = {} or Y = {} ) & not [:X,Y:] = {} ) ; :: thesis: contradiction
then consider z being set such that
A5: z in [:X,Y:] by XBOOLE_0:7;

A6: now

assume A7: Y = {} ; :: thesis: contradiction
ex x, y being set st
( x in X & y in Y & [x,y] = z ) by A5, Def2;
hence contradiction by A7; :: thesis: verum

end;

now

assume A8: X = {} ; :: thesis: contradiction
ex x, y being set st
( x in X & y in Y & [x,y] = z ) by A5, Def2;
hence contradiction by A8; :: thesis: verum

end;

hence contradiction by A4, A6; :: thesis: verum