let z, X, Y be set ; :: thesis: ( not {z} = X \/ Y or ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )
assume A1: {z} = X \/ Y ; :: thesis: ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )
then A2: ( X c= {z} & Y c= {z} ) by XBOOLE_1:7;
( X <> {} or Y <> {} ) by A1;
hence ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) ) by A2, Lm3; :: thesis: verum