let A, B be set ; :: thesis: ( ( for x being set st x in A holds
ex K being set st
( K c= B & x c= union K ) ) implies union A c= union B )
assume A1: for x being set st x in A holds
ex K being set st
( K c= B & x c= union K ) ; :: thesis: union A c= union B
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union A or a in union B )
assume a in union A ; :: thesis: a in union B
then consider Z being set such that
A2: a in Z and
A3: Z in A by TARSKI:def 4;
consider K being set such that
A4: K c= B and
A5: Z c= union K by A1, A3;
ex S being set st
( a in S & S in K ) by A2, A5, TARSKI:def 4;
hence a in union B by A4, TARSKI:def 4; :: thesis: verum