begin
theorem Th1:
theorem Th2:
definition
let X be
set ;
let A1,
A2 be
SetSequence of
X;
func A1 (/\) A2 -> SetSequence of
X means :
Def1:
for
n being
Element of
NAT holds
it . n = (A1 . n) /\ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) /\ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) /\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) /\ (A1 . n)
;
func A1 (\/) A2 -> SetSequence of
X means :
Def2:
for
n being
Element of
NAT holds
it . n = (A1 . n) \/ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \/ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \/ (A1 . n)
;
func A1 (\) A2 -> SetSequence of
X means :
Def3:
for
n being
Element of
NAT holds
it . n = (A1 . n) \ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \ (A2 . n) ) holds
b1 = b2
func A1 (\+\) A2 -> SetSequence of
X means :
Def4:
for
n being
Element of
NAT holds
it . n = (A1 . n) \+\ (A2 . n);
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n)
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) & ( for n being Element of NAT holds b2 . n = (A1 . n) \+\ (A2 . n) ) holds
b1 = b2
commutativity
for b1, A1, A2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) \+\ (A2 . n) ) holds
for n being Element of NAT holds b1 . n = (A2 . n) \+\ (A1 . n)
;
end;
:: deftheorem Def1 defines (/\) SETLIM_2:def 1 :
for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (/\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) /\ (A2 . n) );
:: deftheorem Def2 defines (\/) SETLIM_2:def 2 :
for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\/) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \/ (A2 . n) );
:: deftheorem Def3 defines (\) SETLIM_2:def 3 :
for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \ (A2 . n) );
:: deftheorem Def4 defines (\+\) SETLIM_2:def 4 :
for X being set
for A1, A2, b4 being SetSequence of X holds
( b4 = A1 (\+\) A2 iff for n being Element of NAT holds b4 . n = (A1 . n) \+\ (A2 . n) );
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
:: deftheorem Def5 defines (/\) SETLIM_2:def 5 :
for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (/\) A1 iff for n being Element of NAT holds b4 . n = A /\ (A1 . n) );
:: deftheorem Def6 defines (\/) SETLIM_2:def 6 :
for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\/) A1 iff for n being Element of NAT holds b4 . n = A \/ (A1 . n) );
:: deftheorem Def7 defines (\) SETLIM_2:def 7 :
for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\) A1 iff for n being Element of NAT holds b4 . n = A \ (A1 . n) );
:: deftheorem Def8 defines (\) SETLIM_2:def 8 :
for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A1 (\) A iff for n being Element of NAT holds b4 . n = (A1 . n) \ A );
:: deftheorem Def9 defines (\+\) SETLIM_2:def 9 :
for X being set
for A1 being SetSequence of X
for A being Subset of X
for b4 being SetSequence of X holds
( b4 = A (\+\) A1 iff for n being Element of NAT holds b4 . n = A \+\ (A1 . n) );
theorem
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th50:
theorem Th51:
theorem
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem
theorem Th58:
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem