Copyright (c) 2003 Association of Mizar Users
environ
vocabulary BOOLE;
notation TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1;
constructors TARSKI, SUBSET_1, XBOOLE_0;
clusters SUBSET_1, ZFMISC_1, XBOOLE_0;
theorems TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1;
begin
:: This file contains statements which are obvious for Mizar checker if
:: "requirements SUBSET" is included in the environment description
:: of an article. They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Some of these items need also "requirements BOOLE" for proper work.
theorem Th1:
for a, b being set holds
a in b implies a is Element of b
proof
let a, b be set;
assume
A1: a in b;
then b <> {} by XBOOLE_0:def 1;
then b is non empty by XBOOLE_0:def 5;
hence a is Element of b by A1,SUBSET_1:def 2;
end;
theorem :: requirements BOOLE also needed
for a, b being set holds
a is Element of b & b is non empty implies a in b by SUBSET_1:def 2;
theorem Th3:
for a, b being set holds
a is Element of bool b iff a c= b
proof
let a, b be set;
hereby assume a is Element of bool b;
then a in bool b by SUBSET_1:def 2;
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 2;
end;
theorem
for a, b, c being set holds
a in b & b is Element of bool c implies
a is Element of c
proof
let a, b, c be set;
assume that
A1: a in b and
A2: b is Element of bool c;
b c= c by A2,Th3;
then a in c by A1,TARSKI:def 3;
hence a is Element of c by Th1;
end;
theorem :: requirements BOOLE also needed
for a, b, c being set holds
a in b & b is Element of bool c implies
c is non empty
proof
let a, b, c be set;
assume that
A1: a in b and
A2: b is Element of bool c;
b c= c by A2,Th3;
then a in c by A1,TARSKI:def 3;
then c <> {} by XBOOLE_0:def 1;
hence c is non empty by XBOOLE_0:def 5;
end;