begin
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 ) )
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 ) )
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;
begin
registration
let A be non
empty set ;
coherence
{A} is with_non-empty_elements
let B be non
empty set ;
coherence
{A,B} is with_non-empty_elements
let C be non
empty set ;
coherence
{A,B,C} is with_non-empty_elements
let D be non
empty set ;
coherence
{A,B,C,D} is with_non-empty_elements
let E be non
empty set ;
coherence
{A,B,C,D,E} is with_non-empty_elements
let F be non
empty set ;
coherence
{A,B,C,D,E,F} is with_non-empty_elements
let G be non
empty set ;
coherence
{A,B,C,D,E,F,G} is with_non-empty_elements
let H be non
empty set ;
coherence
{A,B,C,D,E,F,G,H} is with_non-empty_elements
let I be non
empty set ;
coherence
{A,B,C,D,E,F,G,H,I} is with_non-empty_elements
let J be non
empty set ;
coherence
{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements
end;