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