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
A1: ( x in X & X in Rank A ) by TARSKI:def 4;
X c= Rank A by A1, ORDINAL1:def 2;
hence x in Rank A by A1; :: thesis: verum