let U1, U2 be Universe; :: thesis: ( U1 in U2 implies for x being Set of U1 holds x is Set of U2 )
assume A1: U1 in U2 ; :: thesis: for x being Set of U1 holds x is Set of U2
let x be Set of U1; :: thesis: x is Set of U2
x is U1 -set by Def10;
then x is U2 -set by A1, CLASSES4:def 1;
hence x is Set of U2 by Def10; :: thesis: verum