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