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 object such that
A2: x in X by XBOOLE_0:7;
assume Y <> {} ; :: thesis: contradiction
then consider y being object 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 object such that
A5: z in [:X,Y:] by XBOOLE_0:7;
ex x, y being object st
( x in X & y in Y & [x,y] = z ) by A5, Def2;
hence contradiction by A4; :: thesis: verum