subset.miz

    begin

    theorem :: SUBSET:1

    for a,b be set st a in b holds a is Element of b by SUBSET_1:def 1;

    theorem :: SUBSET:2

    for a,b be set st a is Element of b & b is non empty holds a in b by SUBSET_1:def 1;

    theorem :: SUBSET:3



     Th3: for a,b be set holds a is Subset of b iff a c= b

    proof

      let a,b be set;

      hereby

        assume a is Subset of b;

        then a in ( bool b) by SUBSET_1:def 1;

        hence a c= b by ZFMISC_1:def 1;

      end;

      assume a c= b;

      then a in ( bool b) by ZFMISC_1:def 1;

      hence thesis by SUBSET_1:def 1;

    end;

    theorem :: SUBSET:4

    for a,b,c be set st a in b & b is Subset of c holds a is Element of c

    proof

      let a,b,c be set;

      assume that

       A1: a in b and

       A2: b is Subset of c;

      b c= c by A2, Th3;

      then a in c by A1, TARSKI:def 3;

      hence thesis by SUBSET_1:def 1;

    end;

    theorem :: SUBSET:5

    for a,b,c be set st a in b & b is Subset of c holds c is non empty;