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