:: SUBSET semantic presentation begin theorem :: SUBSET:1 for a, b being set st a in b holds a is Element of b by SUBSET_1:def_1; theorem :: SUBSET:2 for a, b being set st a is Element of b & not b is empty holds a in b by SUBSET_1:def_1; theorem Th3: :: SUBSET:3 for a, b being set holds ( a is Subset of b iff a c= b ) proof let a, b be set ; ::_thesis: ( a is Subset of b iff a c= b ) hereby ::_thesis: ( a c= b implies a is Subset of b ) assume a is Subset of b ; ::_thesis: a c= b then a in bool b by SUBSET_1:def_1; hence a c= b by ZFMISC_1:def_1; ::_thesis: verum end; assume a c= b ; ::_thesis: a is Subset of b then a in bool b by ZFMISC_1:def_1; hence a is Subset of b by SUBSET_1:def_1; ::_thesis: verum end; theorem :: SUBSET:4 for a, b, c being set st a in b & b is Subset of c holds a is Element of c proof 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 end; theorem :: SUBSET:5 for a, b, c being set st a in b & b is Subset of c holds not c is empty ;