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

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