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