set A = the Subset of U;
set IT = { the Subset of U};
{ the Subset of U} = Inter ( the Subset of U, the Subset of U) by Th8;
hence ex b₁ being Subset-Family of U ex A, B being Subset of U st b₁ = Inter (A,B) ; :: thesis: verum