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