let F be set ; :: thesis: ( ( for X being set st X in F holds
X is integer-membered ) implies union F is integer-membered )
assume A1: for X being set st X in F holds
X is integer-membered ; :: thesis: union F is integer-membered
let x be set ; :: according to MEMBERED:def 5 :: thesis: ( x in union F implies x is integer )
assume x in union F ; :: thesis: x is integer
then consider X being set such that
A2: x in X and
A3: X in F by TARSKI:def 4;
X is integer-membered by A1, A3;
hence x is integer by A2; :: thesis: verum