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 A1: x in union (Rank A) ; :: thesis: x in Rank A
consider X being set such that
A2: x in X and
A3: X in Rank A by A1, TARSKI:def 4;
A4: X c= Rank A by A3, ORDINAL1:def 2;
thus x in Rank A by A2, A4; :: thesis: verum