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