let X, Y, Z be set ; :: thesis: ( union Y c= Z & X in Y implies X c= Z )
assume that
A1: union Y c= Z and
A2: X in Y ; :: thesis: X c= Z
thus X c= Z :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume x in X ; :: thesis: x in Z
then x in union Y by A2, TARSKI:def 4;
hence x in Z by A1; :: thesis: verum

end;