let W be Universe; :: thesis: for a being Ordinal of W
for L being DOMAIN-Sequence of W holds a in dom L
let a be Ordinal of W; :: thesis: for L being DOMAIN-Sequence of W holds a in dom L
let L be DOMAIN-Sequence of W; :: thesis: a in dom L
a in On W by ORDINAL1:def 9;
hence a in dom L by Def2; :: thesis: verum