let z be object ; :: thesis: for X, Y being set st {z} = X \/ Y & X <> Y & not X = {} holds
Y = {}
let X, Y be set ; :: thesis: ( {z} = X \/ Y & X <> Y & not X = {} implies Y = {} )
assume {z} = X \/ Y ; :: thesis: ( not X <> Y or X = {} or Y = {} )
then ( ( X = {z} & Y = {z} ) or ( X = {} & Y = {z} ) or ( X = {z} & Y = {} ) ) by Th36;
hence ( not X <> Y or X = {} or Y = {} ) ; :: thesis: verum