let X be set ; :: thesis: union (Fin X) = X
union (Fin X) c= union (bool X) by FINSUB_1:13, ZFMISC_1:77;
hence union (Fin X) c= X by ZFMISC_1:81; :: according to XBOOLE_0:def 10 :: thesis: X c= union (Fin X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in union (Fin X) )
assume x in X ; :: thesis: x in union (Fin X)
then {x} c= X by ZFMISC_1:31;
then A1: {x} in Fin X by FINSUB_1:def 5;
x in {x} by TARSKI:def 1;
hence x in union (Fin X) by A1, TARSKI:def 4; :: thesis: verum