let A, B be set ; :: thesis: ( B in [:A,B:] implies ex x being object st
( x in A & B = [x,{x}] ) )
assume B in [:A,B:] ; :: thesis: ex x being object st
( x in A & B = [x,{x}] )
then consider x, y being object such that
A1: ( x in A & y in B & B = [x,y] ) by Th83;
take x ; :: thesis: ( x in A & B = [x,{x}] )
thus x in A by A1; :: thesis: B = [x,{x}]
per cases ( y = {x} or y = {x,y} ) by A1, TARSKI:def 2;
suppose y = {x} ; :: thesis: B = [x,{x}]
hence B = [x,{x}] by A1; :: thesis: verum
end;
suppose A2: y = {x,y} ; :: thesis: B = [x,{x}]
reconsider y = y as set by TARSKI:1;
y in y by TARSKI:def 2, A2;
hence B = [x,{x}] ; :: thesis: verum
end;
end;