let x be set ; :: thesis: ( x U+ {} = [:x,{1}:] & {} U+ x = [:x,{2}:] )
thus x U+ {} = [:x,{1}:] \/ [:{} ,{2}:] by Th74
.= [:x,{1}:] \/ {} by ZFMISC_1:113
.= [:x,{1}:] ; :: thesis: {} U+ x = [:x,{2}:]
thus {} U+ x = [:{} ,{1}:] \/ [:x,{2}:] by Th74
.= {} \/ [:x,{2}:] by ZFMISC_1:113
.= [:x,{2}:] ; :: thesis: verum