:: DYNKIN semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is non empty set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

bool NAT is non empty set

[:NAT,REAL:] is set

bool [:NAT,REAL:] is non empty set

bool (bool REAL) is non empty set

bool NAT is non empty set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V18() ext-real Function-like functional finite V43() V58() set

union {} is epsilon-transitive epsilon-connected ordinal finite set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V18() ext-real Function-like functional finite V43() V58() Element of NAT

1 is non empty epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng E is set

G is set

dom E is set

D is set

E . D is set

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . h is Element of bool Omega

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . D is Element of bool Omega

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . G is Element of bool Omega

Omega is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

Omega + 1 is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

succ Omega is non empty epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() set

{Omega} is non empty finite set

Omega \/ {Omega} is non empty set

Omega is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

Segm Omega is Element of bool NAT

Omega is non empty set

E is Element of Omega

G is Element of Omega

D is Element of Omega

(E,G) followed_by D is Relation-like NAT -defined Omega -valued Function-like V36( NAT ,Omega) Element of bool [:NAT,Omega:]

[:NAT,Omega:] is non empty set

bool [:NAT,Omega:] is non empty set

Omega is non empty set

bool Omega is non empty set

E is Element of bool Omega

G is Element of bool Omega

D is Element of bool Omega

(E,G) followed_by D is Relation-like Function-like set

bool Omega is non empty Element of bool (bool Omega)

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

(E,G) followed_by D is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

Omega is set

E is set

(Omega,E) followed_by {} is Relation-like Function-like set

Union ((Omega,E) followed_by {}) is set

rng ((Omega,E) followed_by {}) is set

union (rng ((Omega,E) followed_by {})) is set

Omega \/ E is set

{Omega,E,{}} is non empty finite set

{Omega,E} is non empty finite set

union {Omega,E} is set

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

G is Element of bool Omega

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

D . G is Element of bool Omega

E . G is Element of bool Omega

G /\ (E . G) is Element of bool Omega

D is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

D . h is Element of bool Omega

E . h is Element of bool Omega

G /\ (E . h) is Element of bool Omega

G . h is Element of bool Omega

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . G is Element of bool Omega

E . D is Element of bool Omega

G is set

D is set

dom E is set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . G is set

E . D is set

dom E is set

E . G is set

E . D is set

dom E is set

Omega is non empty set

meet Omega is set

E is set

G is Element of Omega

D is set

G is set

D is set

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() set

E . G is Element of bool Omega

E | G is Relation-like Function-like set

rng (E | G) is set

union (rng (E | G)) is set

(E . G) \ (union (rng (E | G))) is Element of bool Omega

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() set

G . D is Element of bool Omega

(Omega,E,D) is Element of bool Omega

E . D is Element of bool Omega

E | D is Relation-like Function-like set

rng (E | D) is set

union (rng (E | D)) is set

(E . D) \ (union (rng (E | D))) is Element of bool Omega

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

G . G is Element of bool Omega

(Omega,E,G) is Element of bool Omega

E . G is Element of bool Omega

E | G is Relation-like Function-like set

rng (E | G) is set

union (rng (E | G)) is set

(E . G) \ (union (rng (E | G))) is Element of bool Omega

D . G is Element of bool Omega

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(Omega,E) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() set

(Omega,E) . G is Element of bool Omega

E . G is Element of bool Omega

E | G is Relation-like Function-like set

rng (E | G) is set

union (rng (E | G)) is set

(E . G) \ (union (rng (E | G))) is Element of bool Omega

(Omega,E,G) is Element of bool Omega

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(Omega,E) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

dom E is set

E | D is Relation-like Function-like set

dom (E | D) is set

D /\ NAT is Element of bool REAL

(E | D) . G is set

rng (E | D) is set

E . G is Element of bool Omega

E . D is Element of bool Omega

union (rng (E | D)) is set

(E . D) \ (union (rng (E | D))) is Element of bool Omega

(Omega,E) . D is Element of bool Omega

E | G is Relation-like Function-like set

rng (E | G) is set

union (rng (E | G)) is set

(E . G) \ (union (rng (E | G))) is Element of bool Omega

(Omega,E) . G is Element of bool Omega

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(Omega,E) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng (Omega,E) is set

union (rng (Omega,E)) is set

rng E is set

union (rng E) is set

dom E is set

dom (Omega,E) is set

G is set

D is set

G is set

E . G is set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . h is Element of bool Omega

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() set

E . h is Element of bool Omega

E | h is Relation-like Function-like set

rng (E | h) is set

union (rng (E | h)) is set

x is set

dom (E | h) is set

Y is set

(E | h) . Y is set

X is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . X is Element of bool Omega

(E . h) \ (union (rng (E | h))) is Element of bool Omega

(Omega,E) . h is Element of bool Omega

G is set

D is set

G is set

(Omega,E) . G is set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . h is Element of bool Omega

E | h is Relation-like Function-like set

rng (E | h) is set

union (rng (E | h)) is set

(E . h) \ (union (rng (E | h))) is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

{} Omega is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V18() ext-real Function-like functional finite V43() V58() Element of bool Omega

E is Element of bool Omega

G is Element of bool Omega

(Omega,E,G,({} Omega)) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

bool Omega is non empty Element of bool (bool Omega)

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

D is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D . h is Element of bool Omega

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

0 + 1 is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

D . 0 is Element of bool Omega

D . G is Element of bool Omega

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is Element of bool Omega

(Omega,E,G) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

(Omega,E,G) . D is Element of bool Omega

G is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

(Omega,E,G) . G is Element of bool Omega

E . D is Element of bool Omega

E . G is Element of bool Omega

G /\ (E . D) is Element of bool Omega

G /\ (E . G) is Element of bool Omega

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Union E is Element of bool Omega

rng E is set

union (rng E) is set

G is Element of bool Omega

G /\ (Union E) is Element of bool Omega

(Omega,E,G) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Union (Omega,E,G) is Element of bool Omega

rng (Omega,E,G) is set

union (rng (Omega,E,G)) is set

dom E is set

G is set

D is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng D is set

h is set

dom D is set

h is set

D . h is set

x is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . x is Element of bool Omega

G /\ (E . x) is Element of bool Omega

dom (Omega,E,G) is set

D is set

G is set

h is set

E . h is set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

E . h is Element of bool Omega

G /\ (E . h) is Element of bool Omega

(Omega,E,G) . h is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

bool Omega is non empty Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is non empty Element of bool (bool Omega)

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng G is set

Union G is Element of bool Omega

union (rng G) is set

D is Element of bool Omega

D ` is Element of bool Omega

Omega \ D is set

Omega is non empty set

E is (Omega)

Omega is non empty set

bool Omega is non empty Element of bool (bool Omega)

bool Omega is non empty set

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng E is set

Union E is Element of bool Omega

union (rng E) is set

G is Element of bool Omega

G ` is Element of bool Omega

Omega \ G is set

Omega is non empty set

meet Omega is set

E is non empty set

G is set

bool E is non empty Element of bool (bool E)

bool E is non empty set

bool (bool E) is non empty set

[:NAT,(bool E):] is non empty set

bool [:NAT,(bool E):] is non empty set

G is Relation-like NAT -defined bool E -valued Function-like V36( NAT , bool E) Element of bool [:NAT,(bool E):]

rng G is set

D is set

Union G is Element of bool E

union (rng G) is set

G is Element of bool E

G ` is Element of bool E

E \ G is set

D is set

the Element of Omega is Element of Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is Element of bool Omega

G is Element of bool Omega

E \ G is Element of bool Omega

D is non empty Element of bool (bool Omega)

G ` is Element of bool Omega

Omega \ G is set

E /\ (G `) is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is Element of bool Omega

G is Element of bool Omega

E \/ G is Element of bool Omega

D is non empty Element of bool (bool Omega)

E ` is Element of bool Omega

Omega \ E is set

G ` is Element of bool Omega

Omega \ G is set

(E `) /\ (G `) is Element of bool Omega

(E \/ G) ` is Element of bool Omega

Omega \ (E \/ G) is set

((E \/ G) `) ` is Element of bool Omega

Omega \ ((E \/ G) `) is set

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is non empty Element of bool (bool Omega)

G is finite set

union G is set

D is set

G is set

union G is set

{D} is non empty finite set

G \/ {D} is non empty set

union (G \/ {D}) is set

union {D} is set

h is Element of bool Omega

h is Element of bool Omega

h \/ h is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

bool Omega is non empty Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is non empty Element of bool (bool Omega)

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng G is set

(Omega,G) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng (Omega,G) is set

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

(Omega,G) . D is Element of bool Omega

G | D is Relation-like Function-like set

rng (G | D) is set

dom (G | D) is set

Segm D is finite Element of bool NAT

union (rng (G | D)) is set

dom G is set

G . D is Element of bool Omega

G is Element of bool Omega

(G . D) \ G is Element of bool Omega

D is set

dom (Omega,G) is set

G is set

(Omega,G) . G is set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

(Omega,G) . h is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

bool Omega is non empty Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

E is non empty Element of bool (bool Omega)

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng G is set

union (rng G) is set

(Omega,G) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng (Omega,G) is set

Union (Omega,G) is Element of bool Omega

union (rng (Omega,G)) is set

Omega is non empty set

bool Omega is non empty set

E is non empty (Omega)

D is Element of E

G is Element of E

D \/ G is Element of bool Omega

bool Omega is non empty Element of bool (bool Omega)

bool (bool Omega) is non empty set

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

h is Element of bool Omega

h is Element of bool Omega

{} Omega is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V18() ext-real Function-like functional finite V43() V58() Element of bool Omega

(Omega,h,h,({} Omega)) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

G is Element of E

(Omega,D,G,G) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

[:NAT,E:] is non empty set

bool [:NAT,E:] is non empty set

x is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng x is set

Union x is Element of bool Omega

union (rng x) is set

Omega is non empty set

bool Omega is non empty set

E is non empty (Omega)

G is Element of E

D is Element of E

D \ G is Element of bool Omega

D ` is Element of bool Omega

Omega \ D is set

G \/ (D `) is Element of bool Omega

(G \/ (D `)) ` is Element of bool Omega

Omega \ (G \/ (D `)) is set

G ` is Element of bool Omega

Omega \ G is set

(D `) ` is Element of bool Omega

Omega \ (D `) is set

(G `) /\ ((D `) `) is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is non empty Element of bool (bool Omega)

bool Omega is non empty Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng G is set

Intersection G is Element of bool Omega

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

G . D is Element of bool Omega

(G . D) ` is Element of bool Omega

Omega \ (G . D) is set

Complement G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

D is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

(Complement G) . D is Element of bool Omega

G . D is Element of bool Omega

(G . D) ` is Element of bool Omega

Omega \ (G . D) is set

rng (Complement G) is set

D is set

dom (Complement G) is set

G is set

(Complement G) . G is set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

(Complement G) . h is Element of bool Omega

Union (Complement G) is Element of bool Omega

union (rng (Complement G)) is set

(Union (Complement G)) ` is Element of bool Omega

Omega \ (Union (Complement G)) is set

G is Element of bool Omega

G ` is Element of bool Omega

Omega \ G is set

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is Element of bool (bool Omega)

bool Omega is non empty Element of bool (bool Omega)

bool (bool Omega) is non empty Element of bool (bool (bool Omega))

bool (bool Omega) is non empty set

bool (bool (bool Omega)) is non empty set

G is set

D is non empty set

G is set

meet D is set

G is non empty (Omega)

h is Element of D

h is non empty (Omega)

G is non empty (Omega)

D is non empty (Omega)

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

G is Element of bool Omega

E is set

bool Omega is non empty Element of bool (bool Omega)

D is set

G is set

G is Element of bool (bool Omega)

h is Element of bool Omega

h /\ G is Element of bool Omega

D is Element of bool (bool Omega)

G is Element of bool (bool Omega)

h is Element of bool Omega

h /\ G is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

E is non empty (Omega)

G is Element of E

(Omega,E,G) is Element of bool (bool Omega)

bool (bool Omega) is non empty set

bool Omega is non empty Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty set

bool [:NAT,(bool Omega):] is non empty set

G is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng G is set

Union G is Element of bool Omega

union (rng G) is set

h is set

D is Element of bool Omega

(Omega,G,D) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng (Omega,G,D) is set

h is epsilon-transitive epsilon-connected ordinal natural V18() ext-real V58() Element of NAT

(Omega,G,D) . h is Element of bool Omega

G . h is Element of bool Omega

G /\ (G . h) is Element of bool Omega

(Omega,G,G) is Relation-like NAT -defined bool Omega -valued Function-like V36( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Union (Omega,G,D) is Element of bool Omega

union (rng (Omega,G,D)) is set

G /\ (Union G) is Element of bool Omega

D is Element of bool Omega

D ` is Element of bool Omega

Omega \ D is set

G ` is Element of bool Omega

Omega \ G is set

G /\ (G `) is Element of bool Omega

G /\ D is Element of bool Omega

G \ (G /\ D) is Element of bool Omega

(G /\ D) ` is Element of bool Omega

Omega \ (G /\ D) is set

G /\ ((G /\ D) `) is Element of bool Omega

(G `) \/ (D `) is Element of bool Omega

G /\ ((G `) \/ (D `)) is Element of bool Omega

G /\ (D `) is Element of bool Omega

(G /\ (G `)) \/ (G /\ (D `)) is Element of bool Omega

{} /\ G is finite Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is Element of bool (bool Omega)

(Omega,E) is non empty (Omega)

G is Element of bool Omega

D is Element of bool Omega

G /\ D is Element of bool Omega

G is non empty (Omega)

h is Element of G

(Omega,G,h) is non empty (Omega)

h is set

x is Element of bool Omega

x /\ h is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is Element of bool (bool Omega)

(Omega,E) is non empty (Omega)

G is Element of bool Omega

D is Element of bool Omega

G /\ D is Element of bool Omega

G is non empty (Omega)

bool Omega is non empty Element of bool (bool Omega)

bool (bool Omega) is non empty Element of bool (bool (bool Omega))

bool (bool Omega) is non empty set

bool (bool (bool Omega)) is non empty set

h is set

h is set

x is Element of G

(Omega,G,x) is non empty (Omega)

the Element of G is Element of G

(Omega,G, the Element of G) is non empty (Omega)

(Omega,G,G) is Element of bool (bool Omega)

h is non empty set

meet h is set

x is set

Y is set

X is Element of G

(Omega,G,X) is non empty (Omega)

x /\ X is Element of bool Omega

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is Element of bool (bool Omega)

(Omega,E) is non empty (Omega)

G is Element of bool (bool Omega)

D is set

G is set

D /\ G is set

Omega is non empty set

bool Omega is non empty set

bool (bool Omega) is non empty set

E is Element of bool (bool Omega)

sigma E is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)

(Omega,E) is non empty (Omega)

G is non empty (Omega)

D is non empty (Omega)