let x be set ; :: thesis: ( x <> {} implies x tohilb = id 1 )
assume x <> {} ; :: thesis: x tohilb = id 1
then reconsider xx = x as non empty set ;
xx tohilb = id 1 ;
hence x tohilb = id 1 ; :: thesis: verum