let A, Z be set ; :: thesis: ( ( for X being set st X in A holds
X c= Z ) implies union A c= Z )
assume A1: for X being set st X in A holds
X c= Z ; :: thesis: union A c= Z
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in union A or y in Z )
assume y in union A ; :: thesis: y in Z
then consider Y being set such that
A2: y in Y and
A3: Y in A by TARSKI:def 4;
Y c= Z by A1, A3;
hence y in Z by A2; :: thesis: verum