:: 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)