let z be object ; :: thesis: for X, Y being set holds
( not {z} = X \/ Y or ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) )
let 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 = {} ) )
( X <> {} or Y <> {} ) by A1;
hence ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) ) by A1, Lm3, XBOOLE_1:7; :: thesis: verum