:: SUBSET semantic presentation

theorem Th1: :: SUBSET:1

for a, b being set st a in b holds
a is Element of b

proof end;

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

theorem Th3: :: SUBSET:3

for a, b being set holds
( a is Subset of b iff a c= b )

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

theorem :: SUBSET:5

for a, b, c being set st a in b & b is Subset of c holds
not c is empty

proof end;