let B1, B2 be set ; :: thesis: ( A c= B1 & ( for x, y being set st [x,y] in B1 holds
x c= B1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
B1 c= B ) & A c= B2 & ( for x, y being set st [x,y] in B2 holds
x c= B2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
B2 c= B ) implies B1 = B2 )
assume A1: ( A c= B1 & ( for x, y being set st [x,y] in B1 holds
x c= B1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
B1 c= B ) & A c= B2 & ( for x, y being set st [x,y] in B2 holds
x c= B2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
B2 c= B ) & not B1 = B2 ) ; :: thesis: contradiction
then A2: B1 c= B2 ;
B2 c= B1 by A1;
hence contradiction by A1, A2, XBOOLE_0:def 10; :: thesis: verum