let A be Ordinal; :: thesis: union (Rank A) c= Rank A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (Rank A) or x in Rank A )
assume x in union (Rank A) ; :: thesis: x in Rank A
then consider X being set such that
A2: x in X and
A3: X in Rank A by TARSKI:def 4;
X c= Rank A by A3, ORDINAL1:def 2;
hence x in Rank A by A2; :: thesis: verum