let A be Ordinal; :: thesis: union (Rank A) c= Rank A
let x be object ; :: 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
A1: x in X and
A2: X in Rank A by TARSKI:def 4;
X c= Rank A by A2, ORDINAL1:def 2;
hence x in Rank A by A1; :: thesis: verum