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

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;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