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