let UN be Universe; :: thesis: for x, y being set st x in y & y in UN holds
x in UN
let x, y be set ; :: thesis: ( x in y & y in UN implies x in UN )
assume that
A1: x in y and
A2: y in UN ; :: thesis: x in UN
y c= UN by A2, ORDINAL1:def 2;
hence x in UN by A1; :: thesis: verum