let x be object ; for B being set st B = [x,{x}] holds
B in [:{x},B:]
let B be set ; ( B = [x,{x}] implies B in [:{x},B:] )
assume A1:
B = [x,{x}]
; B in [:{x},B:]
then
[:{x},B:] = {[x,{x}],[x,{x,{x}}]}
by Th29;
hence
B in [:{x},B:]
by TARSKI:def 2, A1; verum