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