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