let U be Universe; :: thesis: for X being Set of U
for Y being set st Y in X holds
Y is Set of U
let X be Set 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 -set by Def10;
then ( Y in union U & U = union U ) by A1, CLASSES4:81, TARSKI:def 4;
then Y is U -set ;
hence Y is Set of U by Def10; :: thesis: verum