let B, A be set ; :: thesis: ( B in [:A,B:] implies ex x being set st
( x in A & B = [x,{x}] ) )
assume B in [:A,B:] ; :: thesis: ex x being set st
( x in A & B = [x,{x}] )
then consider x, y being set such that
A1: ( x in A & y in B & B = [x,y] ) by Th103;
take x ; :: thesis: ( x in A & B = [x,{x}] )
thus x in A by A1; :: thesis: B = [x,{x}]
A2: y in [x,y] by A1;

per cases ( y = {x} or y = {x,y} ) by A2, TARSKI:def 2;

suppose y = {x} ; :: thesis: B = [x,{x}]

hence B = [x,{x}] by A1; :: thesis: verum

end;

suppose y = {x,y} ; :: thesis: B = [x,{x}]

then y in y by TARSKI:def 2;
hence B = [x,{x}] ; :: thesis: verum

end;

end;