let W be Universe; :: thesis: for X being set st X in W holds
sup X in W
let X be set ; :: thesis: ( X in W implies sup X in W )
reconsider a = union (On X) as Ordinal by ORDINAL3:5;
A1: On X c= X by ORDINAL2:7;
assume X in W ; :: thesis: sup X in W
then On X in W by A1, CLASSES1:def 1;
then reconsider a = a as Ordinal of W by CLASSES2:59;
sup X c= succ a by ORDINAL3:72;
hence sup X in W by CLASSES1:def 1; :: thesis: verum