:: HEYTING1 semantic presentation

{} is empty V7() non-empty empty-yielding finite finite-yielding V27() set

the empty V7() non-empty empty-yielding finite finite-yielding V27() set is empty V7() non-empty empty-yielding finite finite-yielding V27() set

1 is non empty set

{{},1} is non empty finite set

K162() is set

bool K162() is non empty cup-closed diff-closed preBoolean set

Fin {} is non empty cup-closed diff-closed preBoolean set

{{}} is non empty finite V27() set

bool {} is non empty finite V27() cup-closed diff-closed preBoolean set

A is non empty set

O is non empty set

[:A,O:] is non empty V7() set

bool [:A,O:] is non empty cup-closed diff-closed preBoolean set

sd is non empty set

[:A,sd:] is non empty V7() set

bool [:A,sd:] is non empty cup-closed diff-closed preBoolean set

F is non empty V7() V10(A) V11(O) Function-like V17(A) quasi_total Element of bool [:A,O:]

dom F is non empty Element of bool A

bool A is non empty cup-closed diff-closed preBoolean set

w is set

F . w is set

A is non empty set

Fin A is non empty cup-closed diff-closed preBoolean set

O is finite Element of Fin A

sd is finite Element of Fin A

F is Element of A

F is set

A is set

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

O is finite Element of Fin (DISJOINT_PAIRS A)

mi O is Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

{ b

( ( not b

A is set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

O is Element of DISJOINT_PAIRS A

{.O.} is non empty finite Element of Fin (DISJOINT_PAIRS A)

F is Element of DISJOINT_PAIRS A

sd is finite Element of Fin (DISJOINT_PAIRS A)

w is Element of DISJOINT_PAIRS A

{O} is non empty V7() V10( Fin A) V11( Fin A) finite Element of bool (DISJOINT_PAIRS A)

bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

the Element of DISJOINT_PAIRS A is Element of DISJOINT_PAIRS A

{ the Element of DISJOINT_PAIRS A} is non empty V7() V10( Fin A) V11( Fin A) finite Element of bool (DISJOINT_PAIRS A)

bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

A is set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

O is Element of DISJOINT_PAIRS A

{O} is non empty finite set

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

A is set

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

O is Element of the carrier of (NormForm A)

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

O is Element of Normal_forms_on A

O ^ O is finite Element of Fin (DISJOINT_PAIRS A)

{ (b

(DISJOINT_PAIRS A) /\ { (b

mi (O ^ O) is Element of Normal_forms_on A

{ b

( ( not b

mi O is Element of Normal_forms_on A

{ b

( ( not b

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

O is Element of Normal_forms_on A

sd is set

F is finite Element of Fin (DISJOINT_PAIRS A)

w is Element of DISJOINT_PAIRS A

pf is Element of DISJOINT_PAIRS A

A is set

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

O is Element of the carrier of (NormForm A)

sd is set

(A,O) is Element of Normal_forms_on A

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set

bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set

bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set

dom (singleton (DISJOINT_PAIRS A)) is non empty V7() V10( Fin A) V11( Fin A) Element of bool (DISJOINT_PAIRS A)

bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

sd is set

F is Element of DISJOINT_PAIRS A

(singleton (DISJOINT_PAIRS A)) . F is finite Element of Fin (DISJOINT_PAIRS A)

(A,F) is non empty finite Element of Normal_forms_on A

(singleton (DISJOINT_PAIRS A)) . sd is set

sd is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

F is Element of DISJOINT_PAIRS A

sd . F is Element of the carrier of (NormForm A)

(A,F) is non empty finite Element of Normal_forms_on A

O is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

sd is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

F is Element of DISJOINT_PAIRS A

O . F is Element of the carrier of (NormForm A)

(A,F) is non empty finite Element of Normal_forms_on A

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

sd . F is Element of the carrier of (NormForm A)

A is set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set

bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

O is Element of DISJOINT_PAIRS A

sd is Element of DISJOINT_PAIRS A

(A) . sd is Element of the carrier of (NormForm A)

(A,sd) is non empty finite Element of Normal_forms_on A

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

A is set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set

bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

O is Element of DISJOINT_PAIRS A

(A) . O is Element of the carrier of (NormForm A)

(A,O) is non empty finite Element of Normal_forms_on A

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

A is set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set

bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]

[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set

bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set

O is Element of DISJOINT_PAIRS A

(A) . O is Element of the carrier of (NormForm A)

(singleton (DISJOINT_PAIRS A)) . O is finite Element of Fin (DISJOINT_PAIRS A)

(A,O) is non empty finite Element of Normal_forms_on A

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

the carrier of (NormForm A) is non empty set

[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set

bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]

[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set

bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set

O is Element of Normal_forms_on A

FinJoin (O,(A)) is Element of the carrier of (NormForm A)

FinUnion (O,(singleton (DISJOINT_PAIRS A))) is finite Element of Fin (DISJOINT_PAIRS A)

mi (FinUnion (O,(singleton (DISJOINT_PAIRS A)))) is Element of Normal_forms_on A

{ b

( ( not b

sd is Element of DISJOINT_PAIRS A

F is Element of DISJOINT_PAIRS A

(singleton (DISJOINT_PAIRS A)) . F is finite Element of Fin (DISJOINT_PAIRS A)

w is Element of DISJOINT_PAIRS A

pf is Element of DISJOINT_PAIRS A

(singleton (DISJOINT_PAIRS A)) . pf is finite Element of Fin (DISJOINT_PAIRS A)

[:(Fin (DISJOINT_PAIRS A)),(Normal_forms_on A):] is non empty V7() set

bool [:(Fin (DISJOINT_PAIRS A)),(Normal_forms_on A):] is non empty cup-closed diff-closed preBoolean set

sd is non empty V7() V10( Fin (DISJOINT_PAIRS A)) V11( Normal_forms_on A) Function-like V17( Fin (DISJOINT_PAIRS A)) quasi_total Element of bool [:(Fin (DISJOINT_PAIRS A)),(Normal_forms_on A):]

[:(Fin (DISJOINT_PAIRS A)), the carrier of (NormForm A):] is non empty V7() set

bool [:(Fin (DISJOINT_PAIRS A)), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

F is non empty V7() V10( Fin (DISJOINT_PAIRS A)) V11( the carrier of (NormForm A)) Function-like V17( Fin (DISJOINT_PAIRS A)) quasi_total Element of bool [:(Fin (DISJOINT_PAIRS A)), the carrier of (NormForm A):]

{}. (DISJOINT_PAIRS A) is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin (DISJOINT_PAIRS A)

F . ({}. (DISJOINT_PAIRS A)) is Element of the carrier of (NormForm A)

mi ({}. (DISJOINT_PAIRS A)) is Element of Normal_forms_on A

{ b

( ( not b

Bottom (NormForm A) is Element of the carrier of (NormForm A)

the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]

[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set

[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set

bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

the_unity_wrt the L_join of (NormForm A) is Element of the carrier of (NormForm A)

w is finite Element of Fin (DISJOINT_PAIRS A)

F . w is Element of the carrier of (NormForm A)

(A,(F . w)) is Element of Normal_forms_on A

mi w is Element of Normal_forms_on A

{ b

( ( not b

pf is finite Element of Fin (DISJOINT_PAIRS A)

F . pf is Element of the carrier of (NormForm A)

(A,(F . pf)) is Element of Normal_forms_on A

mi pf is Element of Normal_forms_on A

{ b

( ( not b

w \/ pf is finite Element of Fin (DISJOINT_PAIRS A)

F . (w \/ pf) is Element of the carrier of (NormForm A)

mi (w \/ pf) is Element of Normal_forms_on A

{ b

( ( not b

(mi w) \/ pf is finite Element of Fin (DISJOINT_PAIRS A)

mi ((mi w) \/ pf) is Element of Normal_forms_on A

{ b

( ( not b

(mi w) \/ (mi pf) is finite Element of Fin (DISJOINT_PAIRS A)

mi ((mi w) \/ (mi pf)) is Element of Normal_forms_on A

{ b

( ( not b

the L_join of (NormForm A) . ((F . w),(F . pf)) is Element of the carrier of (NormForm A)

F * (singleton (DISJOINT_PAIRS A)) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

w is Element of DISJOINT_PAIRS A

(F * (singleton (DISJOINT_PAIRS A))) . w is Element of the carrier of (NormForm A)

(singleton (DISJOINT_PAIRS A)) . w is finite Element of Fin (DISJOINT_PAIRS A)

F . ((singleton (DISJOINT_PAIRS A)) . w) is Element of the carrier of (NormForm A)

(A,w) is non empty finite Element of Normal_forms_on A

F . (A,w) is Element of the carrier of (NormForm A)

mi (A,w) is Element of Normal_forms_on A

{ b

( ( not b

(A) . w is Element of the carrier of (NormForm A)

the L_join of (NormForm A) $$ (O,(A)) is Element of the carrier of (NormForm A)

the L_join of (NormForm A) $$ (O,(F * (singleton (DISJOINT_PAIRS A)))) is Element of the carrier of (NormForm A)

F . (FinUnion (O,(singleton (DISJOINT_PAIRS A)))) is Element of the carrier of (NormForm A)

A is set

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

(A) is non empty V7() V10( DISJOINT_PAIRS A) V11( the carrier of (NormForm A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):]

[:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty V7() set

bool [:(DISJOINT_PAIRS A), the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

O is Element of the carrier of (NormForm A)

(A,O) is Element of Normal_forms_on A

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

FinJoin ((A,O),(A)) is Element of the carrier of (NormForm A)

singleton (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( Fin (DISJOINT_PAIRS A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):]

[:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty V7() set

bool [:(DISJOINT_PAIRS A),(Fin (DISJOINT_PAIRS A)):] is non empty cup-closed diff-closed preBoolean set

FinUnion ((A,O),(singleton (DISJOINT_PAIRS A))) is finite Element of Fin (DISJOINT_PAIRS A)

A is set

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

O is Element of the carrier of (NormForm A)

sd is Element of the carrier of (NormForm A)

O "\/" sd is Element of the carrier of (NormForm A)

the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]

[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set

[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set

bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

the L_join of (NormForm A) . (O,sd) is Element of the carrier of (NormForm A)

(A,O) is Element of Normal_forms_on A

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

(A,sd) is Element of Normal_forms_on A

(A,O) \/ (A,sd) is finite Element of Fin (DISJOINT_PAIRS A)

mi ((A,O) \/ (A,sd)) is Element of Normal_forms_on A

{ b

( ( not b

F is Element of [:(Fin A),(Fin A):]

w is Element of DISJOINT_PAIRS A

O \/ sd is set

pf is Element of DISJOINT_PAIRS A

A is set

NormForm A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded LattStr

the carrier of (NormForm A) is non empty set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

O is Element of the carrier of (NormForm A)

sd is Element of the carrier of (NormForm A)

(A,O) is Element of Normal_forms_on A

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

(A,sd) is Element of Normal_forms_on A

(A,O) \/ (A,sd) is finite Element of Fin (DISJOINT_PAIRS A)

mi ((A,O) \/ (A,sd)) is Element of Normal_forms_on A

{ b

( ( not b

F is Element of DISJOINT_PAIRS A

O \/ sd is set

w is Element of DISJOINT_PAIRS A

F is Element of DISJOINT_PAIRS A

mi (A,sd) is Element of Normal_forms_on A

{ b

( ( not b

w is Element of DISJOINT_PAIRS A

O \/ sd is set

pf is Element of DISJOINT_PAIRS A

O "\/" sd is Element of the carrier of (NormForm A)

the L_join of (NormForm A) is non empty V7() V10([: the carrier of (NormForm A), the carrier of (NormForm A):]) V11( the carrier of (NormForm A)) Function-like V17([: the carrier of (NormForm A), the carrier of (NormForm A):]) quasi_total having_a_unity commutative associative idempotent Element of bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):]

[: the carrier of (NormForm A), the carrier of (NormForm A):] is non empty V7() set

[:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty V7() set

bool [:[: the carrier of (NormForm A), the carrier of (NormForm A):], the carrier of (NormForm A):] is non empty cup-closed diff-closed preBoolean set

the L_join of (NormForm A) . (O,sd) is Element of the carrier of (NormForm A)

A is set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set

[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set

bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set

O is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]

sd is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]

F is Element of [:(Fin A),(Fin A):]

w is Element of [:(Fin A),(Fin A):]

O . (F,w) is Element of [:(Fin A),(Fin A):]

F \ w is Element of [:(Fin A),(Fin A):]

F `1 is finite Element of Fin A

w `1 is finite Element of Fin A

(F `1) \ (w `1) is finite Element of Fin A

F `2 is finite Element of Fin A

w `2 is finite Element of Fin A

(F `2) \ (w `2) is finite Element of Fin A

[((F `1) \ (w `1)),((F `2) \ (w `2))] is V1() Element of [:(Fin A),(Fin A):]

{((F `1) \ (w `1)),((F `2) \ (w `2))} is non empty finite V27() set

{((F `1) \ (w `1))} is non empty finite V27() set

{{((F `1) \ (w `1)),((F `2) \ (w `2))},{((F `1) \ (w `1))}} is non empty finite V27() set

sd . (F,w) is Element of [:(Fin A),(Fin A):]

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

(A) is non empty set

Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)

O is finite Element of Fin (DISJOINT_PAIRS A)

{ [ { (b

( not b

(DISJOINT_PAIRS A) /\ { [ { (b

( not b

{ ((b

union { ((b

{ (a

{ (a

[ { (a

{ { (a

{ { (a

{{ { (a

{ H

( not b

{ H

(DISJOINT_PAIRS A) /\ { H

( not b

pf is set

sf is Element of DISJOINT_PAIRS A

sf `1 is finite Element of Fin A

sf `2 is finite Element of Fin A

(sf `1) \/ (sf `2) is finite Element of Fin A

pf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))

sf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))

pf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11((A)) Function-like finite Element of bool [:(DISJOINT_PAIRS A),(A):]

[:(DISJOINT_PAIRS A),(A):] is non empty V7() set

bool [:(DISJOINT_PAIRS A),(A):] is non empty cup-closed diff-closed preBoolean set

sf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11((A)) Function-like finite Element of bool [:(DISJOINT_PAIRS A),(A):]

a is Element of DISJOINT_PAIRS A

pf . a is set

a `1 is set

sf . a is set

{ (pf . b

{ (sf . b

a is Element of DISJOINT_PAIRS A

pf . a is set

a `2 is set

sf . a is set

{ (pf . b

{ (sf . b

{ (pf . b

{ (pf . b

[ { (pf . b

{ { (pf . b

{ { (pf . b

{{ { (pf . b

{ (sf . b

{ (sf . b

[ { (sf . b

{ { (sf . b

{ { (sf . b

{{ { (sf . b

pf is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))

pf .: O is finite set

sf is set

pf .: O is finite Element of Fin (A)

Fin (A) is non empty cup-closed diff-closed preBoolean set

dom pf is V7() V10( Fin A) V11( Fin A) Element of bool (DISJOINT_PAIRS A)

bool (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

a is set

pf . a is set

v is Element of DISJOINT_PAIRS A

v `1 is finite Element of Fin A

v `2 is finite Element of Fin A

(v `1) \/ (v `2) is finite Element of Fin A

pf . v is Element of (A)

{ H

{ H

{ H

Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]

(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]

[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set

[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set

bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set

incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set

bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set

sd is finite Element of Fin (DISJOINT_PAIRS A)

{ (FinPairUnion (O,((A) .: (b

(DISJOINT_PAIRS A) /\ { (FinPairUnion (O,((A) .: (b

pf is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])

pf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

sf is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])

sf | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

(A) .: (pf,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

((A) .: (pf,(incl (DISJOINT_PAIRS A)))) | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

(A) .: (sf,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

((A) .: (sf,(incl (DISJOINT_PAIRS A)))) | O is V7() V10( DISJOINT_PAIRS A) V10(O) V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like finite Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

FinPairUnion (O,((A) .: (pf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

FinPairUnion A is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total commutative associative idempotent Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]

(FinPairUnion A) $$ (O,((A) .: (pf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

FinPairUnion (O,((A) .: (sf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

(FinPairUnion A) $$ (O,((A) .: (sf,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

{ H

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

(A) is non empty set

Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)

O is finite Element of Fin (DISJOINT_PAIRS A)

(A,O) is finite Element of Fin (DISJOINT_PAIRS A)

{ [ { (b

( not b

(DISJOINT_PAIRS A) /\ { [ { (b

( not b

sd is Element of DISJOINT_PAIRS A

F is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))

{ (F . b

{ (F . b

[ { (F . b

{ { (F . b

{ { (F . b

{{ { (F . b

[{},{}] is V1() set

{{},{}} is non empty finite V27() set

{{{},{}},{{}}} is non empty finite V27() set

A is set

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

{}. A is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin A

[({}. A),({}. A)] is V1() Element of [:(Fin A),(Fin A):]

{({}. A),({}. A)} is non empty finite V27() set

{({}. A)} is non empty finite V27() set

{{({}. A),({}. A)},{({}. A)}} is non empty finite V27() set

[{},{}] `1 is set

[{},{}] `2 is set

{[{},{}]} is non empty V7() finite set

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

O is Element of Normal_forms_on A

(A,O) is finite Element of Fin (DISJOINT_PAIRS A)

(A) is non empty set

Funcs ((DISJOINT_PAIRS A),(A)) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,(A)

{ [ { (b

( not b

(DISJOINT_PAIRS A) /\ { [ { (b

( not b

sd is set

F is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))

{ (F . b

{ (F . b

[ { (F . b

{ { (F . b

{ { (F . b

{{ { (F . b

sd `2 is set

the Element of sd `2 is Element of sd `2

pf is Element of DISJOINT_PAIRS A

F . pf is Element of (A)

pf `1 is finite Element of Fin A

sd `1 is set

the Element of sd `1 is Element of sd `1

pf is Element of DISJOINT_PAIRS A

F . pf is Element of (A)

pf `2 is finite Element of Fin A

the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) is V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A))

F is set

{ ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b

the Element of { ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b

pf is Element of DISJOINT_PAIRS A

the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . pf is Element of (A)

pf `2 is finite Element of Fin A

{ ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b

the Element of { ( the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . b

pf is Element of DISJOINT_PAIRS A

the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . pf is Element of (A)

pf `1 is finite Element of Fin A

w is Element of DISJOINT_PAIRS A

the V7() V10( DISJOINT_PAIRS A) V11((A)) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),(A)) . w is Element of (A)

w `1 is finite Element of Fin A

w `2 is finite Element of Fin A

(w `1) \/ (w `2) is finite Element of Fin A

A is set

DISJOINT_PAIRS A is non empty V7() V10( Fin A) V11( Fin A) Element of bool [:(Fin A),(Fin A):]

Fin A is non empty cup-closed diff-closed preBoolean set

[:(Fin A),(Fin A):] is non empty V7() set

bool [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

{ b

Fin (DISJOINT_PAIRS A) is non empty cup-closed diff-closed preBoolean set

Normal_forms_on A is non empty Element of bool (Fin (DISJOINT_PAIRS A))

bool (Fin (DISJOINT_PAIRS A)) is non empty cup-closed diff-closed preBoolean set

{ b

( not b

O is Element of Normal_forms_on A

sd is Element of Normal_forms_on A

(A,O,sd) is finite Element of Fin (DISJOINT_PAIRS A)

Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is non empty functional FUNCTION_DOMAIN of DISJOINT_PAIRS A,[:(Fin A),(Fin A):]

(A) is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]

[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:] is non empty V7() set

[:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty V7() set

bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set

incl (DISJOINT_PAIRS A) is non empty V7() V10( DISJOINT_PAIRS A) V11( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

[:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty V7() set

bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:] is non empty cup-closed diff-closed preBoolean set

{ (FinPairUnion (O,((A) .: (b

(DISJOINT_PAIRS A) /\ { (FinPairUnion (O,((A) .: (b

{}. A is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin A

{}. (DISJOINT_PAIRS A) is empty V7() non-empty empty-yielding finite finite-yielding V27() Element of Fin (DISJOINT_PAIRS A)

F is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])

(A) .: (F,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

FinPairUnion (O,((A) .: (F,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

FinPairUnion A is non empty V7() V10([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) V11([:(Fin A),(Fin A):]) Function-like V17([:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:]) quasi_total commutative associative idempotent Element of bool [:[:[:(Fin A),(Fin A):],[:(Fin A),(Fin A):]:],[:(Fin A),(Fin A):]:]

(FinPairUnion A) $$ (O,((A) .: (F,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

the_unity_wrt (FinPairUnion A) is Element of [:(Fin A),(Fin A):]

F is set

w is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])

(A) .: (w,(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

FinPairUnion (O,((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

(FinPairUnion A) $$ (O,((A) .: (w,(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

w .: O is finite Element of Fin [:(Fin A),(Fin A):]

Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) is V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])

w is set

(A) .: ( the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))) is non empty V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of bool [:(DISJOINT_PAIRS A),[:(Fin A),(Fin A):]:]

FinPairUnion (O,((A) .: ( the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

(FinPairUnion A) $$ (O,((A) .: ( the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A))))) is Element of [:(Fin A),(Fin A):]

the V7() V10( DISJOINT_PAIRS A) V11([:(Fin A),(Fin A):]) Function-like V17( DISJOINT_PAIRS A) quasi_total Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) .: O is finite Element of Fin [:(Fin A),(Fin A):]

Fin [:(Fin A),(Fin A):] is non empty cup-closed diff-closed preBoolean set

[:(Fin {}),(Fin {}):] is non empty V7() set

DISJOINT_PAIRS {} is non empty V7() V10( Fin {}) V11( Fin {}) Element of bool [:(Fin {}),(Fin {}):]

bool [:(Fin {}),(Fin {}):] is non empty cup-closed diff-closed preBoolean set

{ b