let U be Universe; :: thesis: for X being class of U
for Y being set st Y in X holds
Y is Set of U
let X be class of U; :: thesis: for Y being set st Y in X holds
Y is Set of U
let Y be set ; :: thesis: ( Y in X implies Y is Set of U )
assume A1: Y in X ; :: thesis: Y is Set of U
X is U -Class by Def12;
then Y is U -set by A1;
hence Y is Set of U by Def10; :: thesis: verum