:: DYNKIN semantic presentation

REAL is set

bool REAL is non empty set

bool NAT is non empty set

bool is non empty set
bool () is non empty set
bool NAT is non empty 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):]
rng E is set
G is set
dom E is set
D is set
E . D is set

E . h is Element of bool Omega

E . D is Element of bool Omega

E . G is Element of bool Omega

{Omega} is non empty finite set
Omega \/ {Omega} is non empty set

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

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

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

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

E . G is Element of bool Omega
E . D is Element of bool Omega
G is set
D is set
dom E is set

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

E . G is Element of bool Omega

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

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

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 . G is Element of bool Omega
(Omega,E,G) is Element of bool Omega
E . G is Element of bool Omega

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

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

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

dom E is 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

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

E . h is Element of bool Omega

E . h is Element of bool Omega

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

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

E . h is Element of bool Omega

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

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

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

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

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

(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 /\ () 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

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

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

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

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

rng (G | D) is set
dom (G | D) is set

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

(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,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

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 Element of bool Omega
G . D is Element of bool Omega
(G . D) ` is Element of bool Omega
Omega \ (G . D) is set
rng () is set
D is set
dom () is set
G is set
() . G is set

() . h is Element of bool Omega
Union () is Element of bool Omega
union (rng ()) is set
(Union ()) ` is Element of bool Omega
Omega \ (Union ()) 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

(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 /\ () 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)