let a, b, c be set ; :: thesis: ( a in b & b is Subset of c implies a is Element of c )
assume that
A1: a in b and
A2: b is Subset of c ; :: thesis: a is Element of c
b c= c by A2, Th3;
then a in c by A1, TARSKI:def 3;
hence a is Element of c by SUBSET_1:def 1; :: thesis: verum