let U1, U2 be Universe; :: thesis: ( U1 in U2 implies for x being object st x is U1 -Class holds
x is U2 -set )
assume A1: U1 in U2 ; :: thesis: for x being object st x is U1 -Class holds
x is U2 -set
let x be object ; :: thesis: ( x is U1 -Class implies x is U2 -set )
assume A2: x is U1 -Class ; :: thesis: x is U2 -set
bool U1 in U2 by A1, CLASSES4:def 3;
hence x is U2 -set by A2, CLASSES4:def 1; :: thesis: verum