let a be Ordinal; :: thesis: for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds sup f in U
let U be Universe; :: thesis: ( a in U implies for f being Ordinal-Sequence of a,U holds sup f in U )
assume A1: a in U ; :: thesis: for f being Ordinal-Sequence of a,U holds sup f in U
let f be Ordinal-Sequence of a,U; :: thesis: sup f in U
reconsider u = Union f as Ordinal of U by Th41, A1;
On (rng f) = rng f by Th2;
then sup f c= succ u by ORDINAL3:72;
hence sup f in U by CLASSES1:def 1; :: thesis: verum