:: RPR_1 semantic presentation

REAL is V33() V34() V35() V39() set
NAT is V5() V9() V33() V34() V35() V36() V37() V38() V39() non finite cardinal limit_cardinal Element of K11(REAL)
K11(REAL) is non empty set
NAT is V5() V9() V33() V34() V35() V36() V37() V38() V39() non finite cardinal limit_cardinal set
K11(NAT) is non empty V5() non finite set
K11(NAT) is non empty V5() non finite set
{} is ext-real non positive non negative empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() V39() finite V44() cardinal {} -element set
the ext-real non positive non negative empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() V39() finite V44() cardinal {} -element set is ext-real non positive non negative empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() V39() finite V44() cardinal {} -element set
1 is ext-real positive non negative non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card {} is ext-real non positive non negative empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() V39() finite V44() cardinal {} -element set
0 is ext-real non positive non negative empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() V39() finite V44() cardinal {} -element Element of NAT
E is non empty set
K11(E) is non empty set
A is non empty Element of K11(E)
B is set
B2 is set
{B2} is non empty V5() finite 1 -element set
B is set
{B} is non empty V5() finite 1 -element set
E is non empty set
K11(E) is non empty set
A is non empty V5() finite 1 -element Element of K11(E)
E is non empty set
K11(E) is non empty set
A is Element of K11(E)
B is Element of K11(E)
A \/ B is Element of K11(E)
B2 is non empty V5() finite 1 -element Element of K11(E)
E is non empty set
K11(E) is non empty set
A is Element of K11(E)
B is Element of K11(E)
A \/ B is Element of K11(E)
B2 is non empty V5() finite 1 -element Element of K11(E)
E is non empty set
A is Element of E
{A} is non empty V5() finite 1 -element Element of K11(E)
K11(E) is non empty set
E is non empty set
K11(E) is non empty set
A is non empty V5() finite 1 -element Element of K11(E)
B is non empty V5() finite 1 -element Element of K11(E)
E is non empty set
K11(E) is non empty set
A is non empty V5() finite 1 -element Element of K11(E)
the Element of A is Element of A
{ the Element of A} is non empty V5() finite 1 -element Element of K11(A)
K11(A) is non empty finite V44() set
E is non empty set
K11(E) is non empty set
the Element of E is Element of E
{ the Element of E} is non empty V5() finite 1 -element Element of K11(E)
E is non empty set
K11(E) is non empty set
A is non empty V5() finite 1 -element Element of K11(E)
B is Element of E
{B} is non empty V5() finite 1 -element Element of K11(E)
<*B*> is V16() V19( NAT ) V20(E) V21() FinSequence-like FinSequence of E
rng <*B*> is set
len <*B*> is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
E is non empty set
K11(E) is non empty set
A is non empty V5() finite 1 -element Element of K11(E)
B is Element of K11(E)
A /\ B is finite Element of K11(E)
A /\ E is finite Element of K11(E)
B ` is Element of K11(E)
E \ B is set
B \/ (B `) is Element of K11(E)
[#] E is non empty non proper Element of K11(E)
A /\ (B `) is finite Element of K11(E)
(A /\ B) \/ (A /\ (B `)) is finite Element of K11(E)
E is non empty set
K11(E) is non empty set
A is Element of K11(E)
the Element of A is Element of A
B2 is Element of E
{B2} is non empty V5() finite 1 -element Element of K11(E)
E is non empty set
K11(E) is non empty set
A is non empty V5() finite 1 -element Element of K11(E)
B is Element of K11(E)
B ` is Element of K11(E)
E \ B is set
B \/ (B `) is Element of K11(E)
B2 is Element of E
{B2} is non empty V5() finite 1 -element Element of K11(E)
B2 is Element of E
{B2} is non empty V5() finite 1 -element Element of K11(E)
E is non empty set
K11(E) is non empty set
A is non empty V5() finite 1 -element Element of K11(E)
B is non empty V5() finite 1 -element Element of K11(E)
A /\ B is finite Element of K11(E)
E is non empty set
K11(E) is non empty set
A is Element of K11(E)
B is Element of K11(E)
A /\ B is Element of K11(E)
B ` is Element of K11(E)
E \ B is set
A /\ (B `) is Element of K11(E)
A \ B is Element of K11(E)
E is non empty finite set
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
the Element of E is Element of E
{ the Element of E} is non empty V5() finite 1 -element Element of K11(E)
K11(E) is non empty finite V44() set
card { the Element of E} is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
E is finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is non empty V5() finite 1 -element Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
1 / (card E) is ext-real V14() V15() Element of REAL
E is non empty finite set
[#] E is non empty non proper finite Element of K11(E)
K11(E) is non empty finite V44() set
(E,([#] E)) is ext-real V14() V15() Element of REAL
card ([#] E) is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ([#] E)) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
{} E is ext-real non positive non negative empty proper V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() V39() finite V44() cardinal {} -element Element of K11(E)
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(card E) " is ext-real V14() V15() set
(card A) * ((card E) ") is ext-real V14() V15() set
(card E) * ((card E) ") is ext-real V14() V15() set
[#] E is non empty non proper finite Element of K11(E)
(E,([#] E)) is ext-real V14() V15() Element of REAL
card ([#] E) is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ([#] E)) / (card E) is ext-real V14() V15() set
(card E) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(card E) " is ext-real V14() V15() set
(card A) * ((card E) ") is ext-real V14() V15() set
(card B) * ((card E) ") is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
A \/ B is finite Element of K11(E)
(E,(A \/ B)) is ext-real V14() V15() Element of REAL
card (A \/ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \/ B)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A) + (E,B) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
((E,A) + (E,B)) - (E,(A /\ B)) is ext-real V14() V15() Element of REAL
(card E) " is ext-real V14() V15() set
(card A) + (card B) is ext-real V14() V15() set
((card A) + (card B)) - (card (A /\ B)) is ext-real V14() V15() set
(card (A \/ B)) * ((card E) ") is ext-real V14() V15() set
(card A) * ((card E) ") is ext-real V14() V15() set
(card B) * ((card E) ") is ext-real V14() V15() set
(card (A /\ B)) * ((card E) ") is ext-real V14() V15() set
((card B) * ((card E) ")) - ((card (A /\ B)) * ((card E) ")) is ext-real V14() V15() set
((card A) * ((card E) ")) + (((card B) * ((card E) ")) - ((card (A /\ B)) * ((card E) "))) is ext-real V14() V15() set
((card A) * ((card E) ")) + ((card B) * ((card E) ")) is ext-real V14() V15() set
(((card A) * ((card E) ")) + ((card B) * ((card E) "))) - ((card (A /\ B)) * ((card E) ")) is ext-real V14() V15() set
((card A) / (card E)) + ((card B) * ((card E) ")) is ext-real V14() V15() set
(((card A) / (card E)) + ((card B) * ((card E) "))) - ((card (A /\ B)) * ((card E) ")) is ext-real V14() V15() set
((card A) / (card E)) + ((card B) / (card E)) is ext-real V14() V15() set
(((card A) / (card E)) + ((card B) / (card E))) - ((card (A /\ B)) * ((card E) ")) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
A \/ B is finite Element of K11(E)
(E,(A \/ B)) is ext-real V14() V15() Element of REAL
card (A \/ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \/ B)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A) + (E,B) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
((E,A) + (E,B)) - 0 is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
A ` is finite Element of K11(E)
E \ A is finite set
(E,(A `)) is ext-real V14() V15() Element of REAL
card (A `) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A `)) / (card E) is ext-real V14() V15() set
1 - (E,(A `)) is ext-real V14() V15() Element of REAL
1 - (E,A) is ext-real V14() V15() Element of REAL
A \/ (A `) is finite Element of K11(E)
(E,(A \/ (A `))) is ext-real V14() V15() Element of REAL
card (A \/ (A `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \/ (A `))) / (card E) is ext-real V14() V15() set
(E,A) + (E,(A `)) is ext-real V14() V15() Element of REAL
[#] E is non empty non proper finite Element of K11(E)
(E,([#] E)) is ext-real V14() V15() Element of REAL
card ([#] E) is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ([#] E)) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
A \ B is finite Element of K11(E)
(E,(A \ B)) is ext-real V14() V15() Element of REAL
card (A \ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \ B)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,A) - (E,(A /\ B)) is ext-real V14() V15() Element of REAL
(A \ B) \/ (A /\ B) is finite Element of K11(E)
(E,((A \ B) \/ (A /\ B))) is ext-real V14() V15() Element of REAL
card ((A \ B) \/ (A /\ B)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A \ B) \/ (A /\ B))) / (card E) is ext-real V14() V15() set
(E,(A \ B)) + (E,(A /\ B)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
A is finite Element of K11(E)
A \ B is finite Element of K11(E)
(E,(A \ B)) is ext-real V14() V15() Element of REAL
card (A \ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \ B)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A) - (E,B) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
A \/ B is finite Element of K11(E)
(E,(A \/ B)) is ext-real V14() V15() Element of REAL
card (A \/ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \/ B)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A) + (E,B) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
((E,A) + (E,B)) - (E,(A /\ B)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
B is finite Element of K11(E)
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
B ` is finite Element of K11(E)
E \ B is finite set
A /\ (B `) is finite Element of K11(E)
(E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
card (A /\ (B `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B `))) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) + (E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
[#] E is non empty non proper finite Element of K11(E)
A \/ ([#] E) is non empty finite Element of K11(E)
A /\ (A \/ ([#] E)) is finite Element of K11(E)
A /\ ([#] E) is finite Element of K11(E)
B \/ (B `) is finite Element of K11(E)
A /\ (B \/ (B `)) is finite Element of K11(E)
(A /\ B) \/ (A /\ (B `)) is finite Element of K11(E)
(E,((A /\ B) \/ (A /\ (B `)))) is ext-real V14() V15() Element of REAL
card ((A /\ B) \/ (A /\ (B `))) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A /\ B) \/ (A /\ (B `)))) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
B is finite Element of K11(E)
A \/ B is finite Element of K11(E)
(E,(A \/ B)) is ext-real V14() V15() Element of REAL
card (A \/ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \/ B)) / (card E) is ext-real V14() V15() set
B \ A is finite Element of K11(E)
(E,(B \ A)) is ext-real V14() V15() Element of REAL
card (B \ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B \ A)) / (card E) is ext-real V14() V15() set
(E,(A \/ B)) - (E,(B \ A)) is ext-real V14() V15() Element of REAL
A \/ (B \ A) is finite Element of K11(E)
(E,(A \/ (B \ A))) is ext-real V14() V15() Element of REAL
card (A \/ (B \ A)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \/ (B \ A))) / (card E) is ext-real V14() V15() set
(E,A) + (E,(B \ A)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
A ` is finite Element of K11(E)
E \ A is finite set
B is finite Element of K11(E)
(A `) /\ B is finite Element of K11(E)
(E,((A `) /\ B)) is ext-real V14() V15() Element of REAL
card ((A `) /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A `) /\ B)) / (card E) is ext-real V14() V15() set
(E,A) + (E,((A `) /\ B)) is ext-real V14() V15() Element of REAL
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
B ` is finite Element of K11(E)
E \ B is finite set
(B `) /\ A is finite Element of K11(E)
(E,((B `) /\ A)) is ext-real V14() V15() Element of REAL
card ((B `) /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((B `) /\ A)) / (card E) is ext-real V14() V15() set
(E,B) + (E,((B `) /\ A)) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
A /\ (B `) is finite Element of K11(E)
(E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
card (A /\ (B `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B `))) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) + (E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
B /\ (A `) is finite Element of K11(E)
(E,(B /\ (A `))) is ext-real V14() V15() Element of REAL
card (B /\ (A `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ (A `))) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) + (E,(B /\ (A `))) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
A \/ B is finite Element of K11(E)
B2 is finite Element of K11(E)
(A \/ B) \/ B2 is finite Element of K11(E)
(E,((A \/ B) \/ B2)) is ext-real V14() V15() Element of REAL
card ((A \/ B) \/ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A \/ B) \/ B2)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A) + (E,B) is ext-real V14() V15() Element of REAL
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
((E,A) + (E,B)) + (E,B2) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
A /\ B2 is finite Element of K11(E)
(E,(A /\ B2)) is ext-real V14() V15() Element of REAL
card (A /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B2)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) + (E,(A /\ B2)) is ext-real V14() V15() Element of REAL
B /\ B2 is finite Element of K11(E)
(E,(B /\ B2)) is ext-real V14() V15() Element of REAL
card (B /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ B2)) / (card E) is ext-real V14() V15() set
((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2)) is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) + (E,B2)) - (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2))) is ext-real V14() V15() Element of REAL
(A /\ B) /\ B2 is finite Element of K11(E)
(E,((A /\ B) /\ B2)) is ext-real V14() V15() Element of REAL
card ((A /\ B) /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A /\ B) /\ B2)) / (card E) is ext-real V14() V15() set
((((E,A) + (E,B)) + (E,B2)) - (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2)))) + (E,((A /\ B) /\ B2)) is ext-real V14() V15() Element of REAL
(E,(A \/ B)) is ext-real V14() V15() Element of REAL
card (A \/ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \/ B)) / (card E) is ext-real V14() V15() set
(E,(A \/ B)) + (E,B2) is ext-real V14() V15() Element of REAL
(A \/ B) /\ B2 is finite Element of K11(E)
(E,((A \/ B) /\ B2)) is ext-real V14() V15() Element of REAL
card ((A \/ B) /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A \/ B) /\ B2)) / (card E) is ext-real V14() V15() set
((E,(A \/ B)) + (E,B2)) - (E,((A \/ B) /\ B2)) is ext-real V14() V15() Element of REAL
((E,A) + (E,B)) - (E,(A /\ B)) is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) - (E,(A /\ B))) + (E,B2) is ext-real V14() V15() Element of REAL
((((E,A) + (E,B)) - (E,(A /\ B))) + (E,B2)) - (E,((A \/ B) /\ B2)) is ext-real V14() V15() Element of REAL
- (E,(A /\ B)) is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) + (E,B2)) + (- (E,(A /\ B))) is ext-real V14() V15() Element of REAL
(A /\ B2) \/ (B /\ B2) is finite Element of K11(E)
(E,((A /\ B2) \/ (B /\ B2))) is ext-real V14() V15() Element of REAL
card ((A /\ B2) \/ (B /\ B2)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A /\ B2) \/ (B /\ B2))) / (card E) is ext-real V14() V15() set
((((E,A) + (E,B)) + (E,B2)) + (- (E,(A /\ B)))) - (E,((A /\ B2) \/ (B /\ B2))) is ext-real V14() V15() Element of REAL
(E,(A /\ B2)) + (E,(B /\ B2)) is ext-real V14() V15() Element of REAL
(A /\ B2) /\ (B /\ B2) is finite Element of K11(E)
(E,((A /\ B2) /\ (B /\ B2))) is ext-real V14() V15() Element of REAL
card ((A /\ B2) /\ (B /\ B2)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A /\ B2) /\ (B /\ B2))) / (card E) is ext-real V14() V15() set
((E,(A /\ B2)) + (E,(B /\ B2))) - (E,((A /\ B2) /\ (B /\ B2))) is ext-real V14() V15() Element of REAL
((((E,A) + (E,B)) + (E,B2)) + (- (E,(A /\ B)))) - (((E,(A /\ B2)) + (E,(B /\ B2))) - (E,((A /\ B2) /\ (B /\ B2)))) is ext-real V14() V15() Element of REAL
B2 /\ B is finite Element of K11(E)
B2 /\ (B2 /\ B) is finite Element of K11(E)
A /\ (B2 /\ (B2 /\ B)) is finite Element of K11(E)
(E,(A /\ (B2 /\ (B2 /\ B)))) is ext-real V14() V15() Element of REAL
card (A /\ (B2 /\ (B2 /\ B))) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B2 /\ (B2 /\ B)))) / (card E) is ext-real V14() V15() set
((E,(A /\ B2)) + (E,(B /\ B2))) - (E,(A /\ (B2 /\ (B2 /\ B)))) is ext-real V14() V15() Element of REAL
((((E,A) + (E,B)) + (E,B2)) + (- (E,(A /\ B)))) - (((E,(A /\ B2)) + (E,(B /\ B2))) - (E,(A /\ (B2 /\ (B2 /\ B))))) is ext-real V14() V15() Element of REAL
B2 /\ B2 is finite Element of K11(E)
(B2 /\ B2) /\ B is finite Element of K11(E)
A /\ ((B2 /\ B2) /\ B) is finite Element of K11(E)
(E,(A /\ ((B2 /\ B2) /\ B))) is ext-real V14() V15() Element of REAL
card (A /\ ((B2 /\ B2) /\ B)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ ((B2 /\ B2) /\ B))) / (card E) is ext-real V14() V15() set
((E,(A /\ B2)) + (E,(B /\ B2))) - (E,(A /\ ((B2 /\ B2) /\ B))) is ext-real V14() V15() Element of REAL
((((E,A) + (E,B)) + (E,B2)) + (- (E,(A /\ B)))) - (((E,(A /\ B2)) + (E,(B /\ B2))) - (E,(A /\ ((B2 /\ B2) /\ B)))) is ext-real V14() V15() Element of REAL
((E,(A /\ B2)) + (E,(B /\ B2))) - (E,((A /\ B) /\ B2)) is ext-real V14() V15() Element of REAL
((((E,A) + (E,B)) + (E,B2)) + (- (E,(A /\ B)))) - (((E,(A /\ B2)) + (E,(B /\ B2))) - (E,((A /\ B) /\ B2))) is ext-real V14() V15() Element of REAL
- (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2))) is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) + (E,B2)) + (- (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2)))) is ext-real V14() V15() Element of REAL
((((E,A) + (E,B)) + (E,B2)) + (- (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2))))) + (E,((A /\ B) /\ B2)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
B2 is finite Element of K11(E)
A \/ B is finite Element of K11(E)
(A \/ B) \/ B2 is finite Element of K11(E)
(E,((A \/ B) \/ B2)) is ext-real V14() V15() Element of REAL
card ((A \/ B) \/ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A \/ B) \/ B2)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A) + (E,B) is ext-real V14() V15() Element of REAL
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
((E,A) + (E,B)) + (E,B2) is ext-real V14() V15() Element of REAL
B /\ B2 is finite Element of K11(E)
A /\ (B /\ B2) is finite Element of K11(E)
(E,(A /\ (B /\ B2))) is ext-real V14() V15() Element of REAL
card (A /\ (B /\ B2)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B /\ B2))) / (card E) is ext-real V14() V15() set
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
A /\ B2 is finite Element of K11(E)
(E,(A /\ B2)) is ext-real V14() V15() Element of REAL
card (A /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B2)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) + (E,(A /\ B2)) is ext-real V14() V15() Element of REAL
(E,(B /\ B2)) is ext-real V14() V15() Element of REAL
card (B /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ B2)) / (card E) is ext-real V14() V15() set
((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2)) is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) + (E,B2)) - (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2))) is ext-real V14() V15() Element of REAL
(A /\ B) /\ B2 is finite Element of K11(E)
(E,((A /\ B) /\ B2)) is ext-real V14() V15() Element of REAL
card ((A /\ B) /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A /\ B) /\ B2)) / (card E) is ext-real V14() V15() set
((((E,A) + (E,B)) + (E,B2)) - (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2)))) + (E,((A /\ B) /\ B2)) is ext-real V14() V15() Element of REAL
((((E,A) + (E,B)) + (E,B2)) - (((E,(A /\ B)) + (E,(A /\ B2))) + (E,(B /\ B2)))) + 0 is ext-real V14() V15() Element of REAL
((E,(A /\ B)) + (E,(A /\ B2))) + 0 is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) + (E,B2)) - (((E,(A /\ B)) + (E,(A /\ B2))) + 0) is ext-real V14() V15() Element of REAL
(E,(A /\ B)) + 0 is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) + (E,B2)) - ((E,(A /\ B)) + 0) is ext-real V14() V15() Element of REAL
(((E,A) + (E,B)) + (E,B2)) - 0 is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A) - (E,B) is ext-real V14() V15() Element of REAL
A \ B is finite Element of K11(E)
(E,(A \ B)) is ext-real V14() V15() Element of REAL
card (A \ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A \ B)) / (card E) is ext-real V14() V15() set
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,A) - (E,(A /\ B)) is ext-real V14() V15() Element of REAL
E is finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
A is finite Element of K11(E)
B /\ A is finite Element of K11(E)
(E,(B /\ A)) is ext-real V14() V15() Element of REAL
card (B /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ A)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,(B /\ A)) / (E,A) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
[#] E is non empty non proper finite Element of K11(E)
A is finite Element of K11(E)
(E,([#] E),A) is ext-real V14() V15() Element of REAL
A /\ ([#] E) is finite Element of K11(E)
(E,(A /\ ([#] E))) is ext-real V14() V15() Element of REAL
card (A /\ ([#] E)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ ([#] E))) / (card E) is ext-real V14() V15() set
(E,([#] E)) is ext-real V14() V15() Element of REAL
card ([#] E) is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ([#] E)) / (card E) is ext-real V14() V15() set
(E,(A /\ ([#] E))) / (E,([#] E)) is ext-real V14() V15() Element of REAL
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
E is non empty finite set
[#] E is non empty non proper finite Element of K11(E)
K11(E) is non empty finite V44() set
(E,([#] E),([#] E)) is ext-real V14() V15() Element of REAL
([#] E) /\ ([#] E) is finite Element of K11(E)
(E,(([#] E) /\ ([#] E))) is ext-real V14() V15() Element of REAL
card (([#] E) /\ ([#] E)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (([#] E) /\ ([#] E))) / (card E) is ext-real V14() V15() set
(E,([#] E)) is ext-real V14() V15() Element of REAL
card ([#] E) is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ([#] E)) / (card E) is ext-real V14() V15() set
(E,(([#] E) /\ ([#] E))) / (E,([#] E)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B) " is ext-real V14() V15() Element of REAL
(E,(A /\ B)) * ((E,B) ") is ext-real V14() V15() Element of REAL
(E,B) * ((E,B) ") is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
B \ A is finite Element of K11(E)
(E,(B \ A)) is ext-real V14() V15() Element of REAL
card (B \ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B \ A)) / (card E) is ext-real V14() V15() set
(E,(B \ A)) / (E,B) is ext-real V14() V15() Element of REAL
1 - ((E,(B \ A)) / (E,B)) is ext-real V14() V15() Element of REAL
(E,(B \ A)) + (E,(A /\ B)) is ext-real V14() V15() Element of REAL
(E,B) - (E,(A /\ B)) is ext-real V14() V15() Element of REAL
((E,B) - (E,(A /\ B))) + (E,(A /\ B)) is ext-real V14() V15() Element of REAL
(E,B) - (E,(B \ A)) is ext-real V14() V15() Element of REAL
((E,B) - (E,(B \ A))) / (E,B) is ext-real V14() V15() Element of REAL
(E,B) / (E,B) is ext-real V14() V15() Element of REAL
((E,B) / (E,B)) - ((E,(B \ A)) / (E,B)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,A) / (E,B) is ext-real V14() V15() Element of REAL
B \ A is finite Element of K11(E)
(E,(B \ A)) is ext-real V14() V15() Element of REAL
card (B \ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B \ A)) / (card E) is ext-real V14() V15() set
(E,(B \ A)) / (E,B) is ext-real V14() V15() Element of REAL
1 - ((E,(B \ A)) / (E,B)) is ext-real V14() V15() Element of REAL
(E,B) - (E,A) is ext-real V14() V15() Element of REAL
((E,B) - (E,A)) / (E,B) is ext-real V14() V15() Element of REAL
1 - (((E,B) - (E,A)) / (E,B)) is ext-real V14() V15() Element of REAL
(E,B) / (E,B) is ext-real V14() V15() Element of REAL
((E,B) / (E,B)) - ((E,A) / (E,B)) is ext-real V14() V15() Element of REAL
1 - (((E,B) / (E,B)) - ((E,A) / (E,B))) is ext-real V14() V15() Element of REAL
1 - ((E,A) / (E,B)) is ext-real V14() V15() Element of REAL
1 - (1 - ((E,A) / (E,B))) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
0 / (E,B) is ext-real V14() V15() Element of REAL
(E,B) " is ext-real V14() V15() Element of REAL
0 * ((E,B) ") is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
(E,A,B) is ext-real V14() V15() Element of REAL
B /\ A is finite Element of K11(E)
(E,(B /\ A)) is ext-real V14() V15() Element of REAL
card (B /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ A)) / (card E) is ext-real V14() V15() set
(E,(B /\ A)) / (E,A) is ext-real V14() V15() Element of REAL
(E,A) * (E,A,B) is ext-real V14() V15() Element of REAL
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B) * (E,B,A) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
A ` is finite Element of K11(E)
E \ A is finite set
(E,B,(A `)) is ext-real V14() V15() Element of REAL
(A `) /\ B is finite Element of K11(E)
(E,((A `) /\ B)) is ext-real V14() V15() Element of REAL
card ((A `) /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A `) /\ B)) / (card E) is ext-real V14() V15() set
(E,((A `) /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
1 - (E,B,(A `)) is ext-real V14() V15() Element of REAL
1 - (E,B,A) is ext-real V14() V15() Element of REAL
A \/ (A `) is finite Element of K11(E)
(A \/ (A `)) /\ B is finite Element of K11(E)
[#] E is non empty non proper finite Element of K11(E)
([#] E) /\ B is finite Element of K11(E)
(A /\ B) \/ ((A `) /\ B) is finite Element of K11(E)
(E,(A /\ B)) + (E,((A `) /\ B)) is ext-real V14() V15() Element of REAL
(E,B,A) * (E,B) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + (E,((A `) /\ B)) is ext-real V14() V15() Element of REAL
(E,B,(A `)) * (E,B) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + ((E,B,(A `)) * (E,B)) is ext-real V14() V15() Element of REAL
(E,B,A) + (E,B,(A `)) is ext-real V14() V15() Element of REAL
((E,B,A) + (E,B,(A `))) * (E,B) is ext-real V14() V15() Element of REAL
(E,B) " is ext-real V14() V15() Element of REAL
(((E,B,A) + (E,B,(A `))) * (E,B)) * ((E,B) ") is ext-real V14() V15() Element of REAL
(E,B) * ((E,B) ") is ext-real V14() V15() Element of REAL
((E,B,A) + (E,B,(A `))) * ((E,B) * ((E,B) ")) is ext-real V14() V15() Element of REAL
((E,B,A) + (E,B,(A `))) * 1 is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
[#] E is non empty non proper finite Element of K11(E)
(E,A,([#] E)) is ext-real V14() V15() Element of REAL
([#] E) /\ A is finite Element of K11(E)
(E,(([#] E) /\ A)) is ext-real V14() V15() Element of REAL
card (([#] E) /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (([#] E) /\ A)) / (card E) is ext-real V14() V15() set
(E,(([#] E) /\ A)) / (E,A) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
A ` is finite Element of K11(E)
E \ A is finite set
(E,A,(A `)) is ext-real V14() V15() Element of REAL
(A `) /\ A is finite Element of K11(E)
(E,((A `) /\ A)) is ext-real V14() V15() Element of REAL
card ((A `) /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A `) /\ A)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,((A `) /\ A)) / (E,A) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
A ` is finite Element of K11(E)
E \ A is finite set
(E,(A `),A) is ext-real V14() V15() Element of REAL
A /\ (A `) is finite Element of K11(E)
(E,(A /\ (A `))) is ext-real V14() V15() Element of REAL
card (A /\ (A `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (A `))) / (card E) is ext-real V14() V15() set
(E,(A `)) is ext-real V14() V15() Element of REAL
card (A `) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A `)) / (card E) is ext-real V14() V15() set
(E,(A /\ (A `))) / (E,(A `)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
A ` is finite Element of K11(E)
E \ A is finite set
(E,B,(A `)) is ext-real V14() V15() Element of REAL
(A `) /\ B is finite Element of K11(E)
(E,((A `) /\ B)) is ext-real V14() V15() Element of REAL
card ((A `) /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A `) /\ B)) / (card E) is ext-real V14() V15() set
(E,((A `) /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
1 - (E,B,(A `)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
B ` is finite Element of K11(E)
E \ B is finite set
(E,(B `),A) is ext-real V14() V15() Element of REAL
A /\ (B `) is finite Element of K11(E)
(E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
card (A /\ (B `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B `))) / (card E) is ext-real V14() V15() set
(E,(B `)) is ext-real V14() V15() Element of REAL
card (B `) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B `)) / (card E) is ext-real V14() V15() set
(E,(A /\ (B `))) / (E,(B `)) is ext-real V14() V15() Element of REAL
1 - (E,B) is ext-real V14() V15() Element of REAL
(E,A) / (1 - (E,B)) is ext-real V14() V15() Element of REAL
1 - 1 is ext-real V14() V15() Element of REAL
(E,B) - 1 is ext-real V14() V15() Element of REAL
- (1 - (E,B)) is ext-real V14() V15() Element of REAL
- (- (1 - (E,B))) is ext-real V14() V15() Element of REAL
(E,A,(B `)) is ext-real V14() V15() Element of REAL
(B `) /\ A is finite Element of K11(E)
(E,((B `) /\ A)) is ext-real V14() V15() Element of REAL
card ((B `) /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((B `) /\ A)) / (card E) is ext-real V14() V15() set
(E,((B `) /\ A)) / (E,A) is ext-real V14() V15() Element of REAL
(E,A) * (E,A,(B `)) is ext-real V14() V15() Element of REAL
(E,(B `)) * (E,(B `),A) is ext-real V14() V15() Element of REAL
(E,A) * 1 is ext-real V14() V15() Element of REAL
(E,(B `)) " is ext-real V14() V15() Element of REAL
(E,A) * ((E,(B `)) ") is ext-real V14() V15() Element of REAL
(E,(B `)) * ((E,(B `)) ") is ext-real V14() V15() Element of REAL
(E,(B `),A) * ((E,(B `)) * ((E,(B `)) ")) is ext-real V14() V15() Element of REAL
(E,(B `),A) * 1 is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
B ` is finite Element of K11(E)
E \ B is finite set
A ` is finite Element of K11(E)
E \ A is finite set
(E,(B `),(A `)) is ext-real V14() V15() Element of REAL
(A `) /\ (B `) is finite Element of K11(E)
(E,((A `) /\ (B `))) is ext-real V14() V15() Element of REAL
card ((A `) /\ (B `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A `) /\ (B `))) / (card E) is ext-real V14() V15() set
(E,(B `)) is ext-real V14() V15() Element of REAL
card (B `) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B `)) / (card E) is ext-real V14() V15() set
(E,((A `) /\ (B `))) / (E,(B `)) is ext-real V14() V15() Element of REAL
1 - (E,B) is ext-real V14() V15() Element of REAL
(E,A) / (1 - (E,B)) is ext-real V14() V15() Element of REAL
1 - ((E,A) / (1 - (E,B))) is ext-real V14() V15() Element of REAL
1 - 1 is ext-real V14() V15() Element of REAL
(E,B) - 1 is ext-real V14() V15() Element of REAL
- (1 - (E,B)) is ext-real V14() V15() Element of REAL
- (- (1 - (E,B))) is ext-real V14() V15() Element of REAL
(E,(B `),A) is ext-real V14() V15() Element of REAL
A /\ (B `) is finite Element of K11(E)
(E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
card (A /\ (B `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B `))) / (card E) is ext-real V14() V15() set
(E,(A /\ (B `))) / (E,(B `)) is ext-real V14() V15() Element of REAL
1 - (E,(B `),A) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
B2 is finite Element of K11(E)
B /\ B2 is finite Element of K11(E)
(E,(B /\ B2)) is ext-real V14() V15() Element of REAL
card (B /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ B2)) / (card E) is ext-real V14() V15() set
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
A /\ B is finite Element of K11(E)
(A /\ B) /\ B2 is finite Element of K11(E)
(E,((A /\ B) /\ B2)) is ext-real V14() V15() Element of REAL
card ((A /\ B) /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A /\ B) /\ B2)) / (card E) is ext-real V14() V15() set
(E,(B /\ B2),A) is ext-real V14() V15() Element of REAL
A /\ (B /\ B2) is finite Element of K11(E)
(E,(A /\ (B /\ B2))) is ext-real V14() V15() Element of REAL
card (A /\ (B /\ B2)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B /\ B2))) / (card E) is ext-real V14() V15() set
(E,(A /\ (B /\ B2))) / (E,(B /\ B2)) is ext-real V14() V15() Element of REAL
(E,B2,B) is ext-real V14() V15() Element of REAL
(E,(B /\ B2)) / (E,B2) is ext-real V14() V15() Element of REAL
(E,(B /\ B2),A) * (E,B2,B) is ext-real V14() V15() Element of REAL
((E,(B /\ B2),A) * (E,B2,B)) * (E,B2) is ext-real V14() V15() Element of REAL
(E,B2,B) * (E,B2) is ext-real V14() V15() Element of REAL
(E,(B /\ B2),A) * (E,(B /\ B2)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B,A) * (E,B) is ext-real V14() V15() Element of REAL
B ` is finite Element of K11(E)
E \ B is finite set
(E,(B `),A) is ext-real V14() V15() Element of REAL
A /\ (B `) is finite Element of K11(E)
(E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
card (A /\ (B `)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ (B `))) / (card E) is ext-real V14() V15() set
(E,(B `)) is ext-real V14() V15() Element of REAL
card (B `) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B `)) / (card E) is ext-real V14() V15() set
(E,(A /\ (B `))) / (E,(B `)) is ext-real V14() V15() Element of REAL
(E,(B `),A) * (E,(B `)) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + ((E,(B `),A) * (E,(B `))) is ext-real V14() V15() Element of REAL
1 - 1 is ext-real V14() V15() Element of REAL
(E,B) - 1 is ext-real V14() V15() Element of REAL
1 - (E,B) is ext-real V14() V15() Element of REAL
- (1 - (E,B)) is ext-real V14() V15() Element of REAL
- (- (1 - (E,B))) is ext-real V14() V15() Element of REAL
(E,(A /\ B)) + (E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + (E,(A /\ (B `))) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
B2 is finite Element of K11(E)
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
B \/ B2 is finite Element of K11(E)
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B,A) * (E,B) is ext-real V14() V15() Element of REAL
(E,B2,A) is ext-real V14() V15() Element of REAL
A /\ B2 is finite Element of K11(E)
(E,(A /\ B2)) is ext-real V14() V15() Element of REAL
card (A /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B2)) / (card E) is ext-real V14() V15() set
(E,(A /\ B2)) / (E,B2) is ext-real V14() V15() Element of REAL
(E,B2,A) * (E,B2) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2)) is ext-real V14() V15() Element of REAL
B2 \ B is finite Element of K11(E)
E \ B is finite Element of K11(E)
B ` is finite Element of K11(E)
E \ B is finite set
(E,(B `)) is ext-real V14() V15() Element of REAL
card (B `) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B `)) / (card E) is ext-real V14() V15() set
1 - (E,B) is ext-real V14() V15() Element of REAL
1 - (1 - (E,B)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
B2 is finite Element of K11(E)
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
B3 is finite Element of K11(E)
(E,B3) is ext-real V14() V15() Element of REAL
card B3 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B3) / (card E) is ext-real V14() V15() set
B \/ B2 is finite Element of K11(E)
(B \/ B2) \/ B3 is finite Element of K11(E)
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B,A) * (E,B) is ext-real V14() V15() Element of REAL
(E,B2,A) is ext-real V14() V15() Element of REAL
A /\ B2 is finite Element of K11(E)
(E,(A /\ B2)) is ext-real V14() V15() Element of REAL
card (A /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B2)) / (card E) is ext-real V14() V15() set
(E,(A /\ B2)) / (E,B2) is ext-real V14() V15() Element of REAL
(E,B2,A) * (E,B2) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2)) is ext-real V14() V15() Element of REAL
(E,B3,A) is ext-real V14() V15() Element of REAL
A /\ B3 is finite Element of K11(E)
(E,(A /\ B3)) is ext-real V14() V15() Element of REAL
card (A /\ B3) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B3)) / (card E) is ext-real V14() V15() set
(E,(A /\ B3)) / (E,B3) is ext-real V14() V15() Element of REAL
(E,B3,A) * (E,B3) is ext-real V14() V15() Element of REAL
(((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2))) + ((E,B3,A) * (E,B3)) is ext-real V14() V15() Element of REAL
B /\ B2 is finite Element of K11(E)
B /\ B3 is finite Element of K11(E)
B2 /\ B3 is finite Element of K11(E)
(B /\ B3) \/ (B2 /\ B3) is finite Element of K11(E)
(B \/ B2) /\ B3 is finite Element of K11(E)
((B \/ B2) \/ B3) /\ A is finite Element of K11(E)
(B \/ B2) /\ A is finite Element of K11(E)
B3 /\ A is finite Element of K11(E)
((B \/ B2) /\ A) \/ (B3 /\ A) is finite Element of K11(E)
(E,((B \/ B2) /\ A)) is ext-real V14() V15() Element of REAL
card ((B \/ B2) /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((B \/ B2) /\ A)) / (card E) is ext-real V14() V15() set
(E,(B3 /\ A)) is ext-real V14() V15() Element of REAL
card (B3 /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B3 /\ A)) / (card E) is ext-real V14() V15() set
(E,((B \/ B2) /\ A)) + (E,(B3 /\ A)) is ext-real V14() V15() Element of REAL
B /\ A is finite Element of K11(E)
B2 /\ A is finite Element of K11(E)
(B /\ A) \/ (B2 /\ A) is finite Element of K11(E)
(E,((B /\ A) \/ (B2 /\ A))) is ext-real V14() V15() Element of REAL
card ((B /\ A) \/ (B2 /\ A)) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((B /\ A) \/ (B2 /\ A))) / (card E) is ext-real V14() V15() set
(E,((B /\ A) \/ (B2 /\ A))) + (E,(B3 /\ A)) is ext-real V14() V15() Element of REAL
(E,(A /\ B)) + (E,(A /\ B2)) is ext-real V14() V15() Element of REAL
((E,(A /\ B)) + (E,(A /\ B2))) + (E,(A /\ B3)) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + (E,(A /\ B2)) is ext-real V14() V15() Element of REAL
(((E,B,A) * (E,B)) + (E,(A /\ B2))) + (E,(A /\ B3)) is ext-real V14() V15() Element of REAL
(((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2))) + (E,(A /\ B3)) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
B2 is finite Element of K11(E)
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
B \/ B2 is finite Element of K11(E)
A is finite Element of K11(E)
(E,A,B) is ext-real V14() V15() Element of REAL
B /\ A is finite Element of K11(E)
(E,(B /\ A)) is ext-real V14() V15() Element of REAL
card (B /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ A)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,(B /\ A)) / (E,A) is ext-real V14() V15() Element of REAL
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B,A) * (E,B) is ext-real V14() V15() Element of REAL
(E,B2,A) is ext-real V14() V15() Element of REAL
A /\ B2 is finite Element of K11(E)
(E,(A /\ B2)) is ext-real V14() V15() Element of REAL
card (A /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B2)) / (card E) is ext-real V14() V15() set
(E,(A /\ B2)) / (E,B2) is ext-real V14() V15() Element of REAL
(E,B2,A) * (E,B2) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2)) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) / (((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2))) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
B2 is finite Element of K11(E)
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
B3 is finite Element of K11(E)
(E,B3) is ext-real V14() V15() Element of REAL
card B3 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B3) / (card E) is ext-real V14() V15() set
B \/ B2 is finite Element of K11(E)
(B \/ B2) \/ B3 is finite Element of K11(E)
A is finite Element of K11(E)
(E,A,B) is ext-real V14() V15() Element of REAL
B /\ A is finite Element of K11(E)
(E,(B /\ A)) is ext-real V14() V15() Element of REAL
card (B /\ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B /\ A)) / (card E) is ext-real V14() V15() set
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,(B /\ A)) / (E,A) is ext-real V14() V15() Element of REAL
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,B,A) * (E,B) is ext-real V14() V15() Element of REAL
(E,B2,A) is ext-real V14() V15() Element of REAL
A /\ B2 is finite Element of K11(E)
(E,(A /\ B2)) is ext-real V14() V15() Element of REAL
card (A /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B2)) / (card E) is ext-real V14() V15() set
(E,(A /\ B2)) / (E,B2) is ext-real V14() V15() Element of REAL
(E,B2,A) * (E,B2) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2)) is ext-real V14() V15() Element of REAL
(E,B3,A) is ext-real V14() V15() Element of REAL
A /\ B3 is finite Element of K11(E)
(E,(A /\ B3)) is ext-real V14() V15() Element of REAL
card (A /\ B3) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B3)) / (card E) is ext-real V14() V15() set
(E,(A /\ B3)) / (E,B3) is ext-real V14() V15() Element of REAL
(E,B3,A) * (E,B3) is ext-real V14() V15() Element of REAL
(((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2))) + ((E,B3,A) * (E,B3)) is ext-real V14() V15() Element of REAL
((E,B,A) * (E,B)) / ((((E,B,A) * (E,B)) + ((E,B2,A) * (E,B2))) + ((E,B3,A) * (E,B3))) is ext-real V14() V15() Element of REAL
E is finite set
K11(E) is non empty finite V44() set
B2 is finite Element of K11(E)
B3 is finite Element of K11(E)
B2 /\ B3 is finite Element of K11(E)
(E,(B2 /\ B3)) is ext-real V14() V15() Element of REAL
card (B2 /\ B3) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B2 /\ B3)) / (card E) is ext-real V14() V15() set
(E,B2) is ext-real V14() V15() Element of REAL
card B2 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B2) / (card E) is ext-real V14() V15() set
(E,B3) is ext-real V14() V15() Element of REAL
card B3 is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B3) / (card E) is ext-real V14() V15() set
(E,B2) * (E,B3) is ext-real V14() V15() Element of REAL
B3 /\ B2 is finite Element of K11(E)
(E,(B3 /\ B2)) is ext-real V14() V15() Element of REAL
card (B3 /\ B2) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B3 /\ B2)) / (card E) is ext-real V14() V15() set
(E,B3) * (E,B2) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,B,A) is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,(A /\ B)) / (E,B) is ext-real V14() V15() Element of REAL
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,A) * (E,B) is ext-real V14() V15() Element of REAL
(E,B) / (E,B) is ext-real V14() V15() Element of REAL
(E,A) * ((E,B) / (E,B)) is ext-real V14() V15() Element of REAL
(E,A) * 1 is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
B is finite Element of K11(E)
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,A) * 0 is ext-real V14() V15() Element of REAL
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
A ` is finite Element of K11(E)
E \ A is finite set
(A `) /\ B is finite Element of K11(E)
(E,((A `) /\ B)) is ext-real V14() V15() Element of REAL
card ((A `) /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card ((A `) /\ B)) / (card E) is ext-real V14() V15() set
B \ A is finite Element of K11(E)
(E,(B \ A)) is ext-real V14() V15() Element of REAL
card (B \ A) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (B \ A)) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,B) - (E,(A /\ B)) is ext-real V14() V15() Element of REAL
1 * (E,B) is ext-real V14() V15() Element of REAL
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,A) * (E,B) is ext-real V14() V15() Element of REAL
(1 * (E,B)) - ((E,A) * (E,B)) is ext-real V14() V15() Element of REAL
1 - (E,A) is ext-real V14() V15() Element of REAL
(1 - (E,A)) * (E,B) is ext-real V14() V15() Element of REAL
(E,(A `)) is ext-real V14() V15() Element of REAL
card (A `) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A `)) / (card E) is ext-real V14() V15() set
(E,(A `)) * (E,B) is ext-real V14() V15() Element of REAL
E is non empty finite set
K11(E) is non empty finite V44() set
A is finite Element of K11(E)
B is finite Element of K11(E)
(E,A) is ext-real V14() V15() Element of REAL
card A is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
card E is ext-real non empty V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card A) / (card E) is ext-real V14() V15() set
(E,B) is ext-real V14() V15() Element of REAL
card B is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card B) / (card E) is ext-real V14() V15() set
A /\ B is finite Element of K11(E)
(E,(A /\ B)) is ext-real V14() V15() Element of REAL
card (A /\ B) is ext-real V9() V13() V14() V15() V33() V34() V35() V36() V37() V38() finite cardinal Element of NAT
(card (A /\ B)) / (card E) is ext-real V14() V15() set
(E,A) * (E,B) is ext-real V14() V15() Element of REAL