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 {z} = X \/ Y ; :: thesis: ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )
then ( ( X <> {} or Y <> {} ) & X c= {z} & Y c= {z} ) by XBOOLE_1:7;
hence ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) ) by Lm3; :: thesis: verum