begin
:: deftheorem Def1 defines meet SETFAM_1:def 1 :
for
X being
set for
b2 being
set holds
( (
X <> {} implies (
b2 = meet X iff for
x being
set holds
(
x in b2 iff for
Y being
set st
Y in X holds
x in Y ) ) ) & ( not
X <> {} implies (
b2 = meet X iff
b2 = {} ) ) );
theorem
canceled;
theorem
theorem Th3:
theorem Th4:
theorem
theorem
theorem Th7:
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines is_finer_than SETFAM_1:def 2 :
:: deftheorem defines is_coarser_than SETFAM_1:def 3 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
definition
let SFX,
SFY be
set ;
func UNION SFX,
SFY -> set means :
Def4:
for
Z being
set holds
(
Z in it iff ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X \/ Y ) );
existence
ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
uniqueness
for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
b1 = b2
commutativity
for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) )
func INTERSECTION SFX,
SFY -> set means :
Def5:
for
Z being
set holds
(
Z in it iff ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X /\ Y ) );
existence
ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )
uniqueness
for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
b1 = b2
commutativity
for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
func DIFFERENCE SFX,
SFY -> set means :
Def6:
for
Z being
set holds
(
Z in it iff ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X \ Y ) );
existence
ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) )
uniqueness
for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines UNION SETFAM_1:def 4 :
for
SFX,
SFY being
set for
b3 being
set holds
(
b3 = UNION SFX,
SFY iff for
Z being
set holds
(
Z in b3 iff ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X \/ Y ) ) );
:: deftheorem Def5 defines INTERSECTION SETFAM_1:def 5 :
for
SFX,
SFY being
set for
b3 being
set holds
(
b3 = INTERSECTION SFX,
SFY iff for
Z being
set holds
(
Z in b3 iff ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X /\ Y ) ) );
:: deftheorem Def6 defines DIFFERENCE SETFAM_1:def 6 :
for
SFX,
SFY being
set for
b3 being
set holds
(
b3 = DIFFERENCE SFX,
SFY iff for
Z being
set holds
(
Z in b3 iff ex
X,
Y being
set st
(
X in SFX &
Y in SFY &
Z = X \ Y ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th44:
:: deftheorem SETFAM_1:def 7 :
canceled;
:: deftheorem Def8 defines COMPLEMENT SETFAM_1:def 8 :
theorem
canceled;
theorem Th46:
theorem
theorem
begin
theorem
theorem
canceled;
theorem Th51:
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines with_non-empty_elements SETFAM_1:def 9 :
registration
let A be non
empty set ;
cluster {A} -> with_non-empty_elements ;
coherence
{A} is with_non-empty_elements
let B be non
empty set ;
cluster {A,B} -> with_non-empty_elements ;
coherence
{A,B} is with_non-empty_elements
let C be non
empty set ;
cluster {A,B,C} -> with_non-empty_elements ;
coherence
{A,B,C} is with_non-empty_elements
let D be non
empty set ;
cluster {A,B,C,D} -> with_non-empty_elements ;
coherence
{A,B,C,D} is with_non-empty_elements
let E be non
empty set ;
cluster {A,B,C,D,E} -> with_non-empty_elements ;
coherence
{A,B,C,D,E} is with_non-empty_elements
let F be non
empty set ;
cluster {A,B,C,D,E,F} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F} is with_non-empty_elements
let G be non
empty set ;
cluster {A,B,C,D,E,F,G} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G} is with_non-empty_elements
let H be non
empty set ;
cluster {A,B,C,D,E,F,G,H} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H} is with_non-empty_elements
let I be non
empty set ;
cluster {A,B,C,D,E,F,G,H,I} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H,I} is with_non-empty_elements
let J be non
empty set ;
cluster {A,B,C,D,E,F,G,H,I,J} -> with_non-empty_elements ;
coherence
{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements
end;
theorem
theorem
:: deftheorem Def10 defines Intersect SETFAM_1:def 10 :
theorem Th58:
theorem
:: deftheorem Def11 defines empty-membered SETFAM_1:def 11 :
:: deftheorem Def12 defines Cover SETFAM_1:def 12 :
theorem
theorem Th61:
:: deftheorem Def13 defines with_proper_subsets SETFAM_1:def 13 :
theorem
theorem