K164() is V44() V45() V46() V50() set
K168() is non empty non trivial V31() V36() cardinal limit_cardinal V44() V45() V46() V47() V48() V49() V50() Element of bool K164()
bool K164() is non empty set
{} is Function-like functional empty trivial V31() V35() V36() V40() cardinal {} -element V44() V45() V46() V47() V48() V49() V50() set
1 is non empty V26() V27() V31() V35() V36() cardinal V44() V45() V46() V47() V48() V49() Element of K168()
{{},1} is non empty V36() V40() V44() V45() V46() V47() V48() V49() set
K156() is non empty non trivial V31() V36() cardinal limit_cardinal V44() V45() V46() V47() V48() V49() V50() set
bool K156() is non empty non trivial V36() set
F is set
[:F,F:] is set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
A is set
F is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) Element of bool [:[:F,F:],F:]
F . A is set
dom F is Relation-like set
rng F is set
F is set
[:F,F:] is set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
bool F is non empty set
A is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) Element of bool [:[:F,F:],F:]
F is Element of bool F
[:F,F:] is set
y is set
A . y is set
F is Relation-like set
A is set
[:A,A:] is set
F | [:A,A:] is Relation-like set
F is Relation-like set
A is set
(F,A) is set
[:A,A:] is set
F | [:A,A:] is Relation-like set
F is Relation-like Function-like set
A is set
(F,A) is Relation-like set
[:A,A:] is set
F | [:A,A:] is Relation-like Function-like set
F is set
[:F,F:] is set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
A is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) Element of bool [:[:F,F:],F:]
F is (F,A)
(A,F) is Relation-like Function-like set
[:F,F:] is set
A | [:F,F:] is Relation-like Function-like set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
dom A is Relation-like set
dom (A,F) is set
y is set
(A,F) . y is set
A . y is set
F is set
[:F,F:] is set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
A is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) Element of bool [:[:F,F:],F:]
F is (F,A)
(A,F) is Relation-like Function-like set
[:F,F:] is set
A | [:F,F:] is Relation-like Function-like set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
F is set
A is set
{A} is non empty trivial V36() 1 -element set
F is set
F \ {A} is Element of bool F
bool F is non empty set
{{}} is non empty trivial V36() V40() 1 -element V44() V45() V46() V47() V48() V49() set
F \ {{}} is Element of bool F
A is set
{A} is non empty trivial V36() 1 -element set
F \ {A} is Element of bool F
F is set
A is V26() V31() V35() V36() cardinal Element of {{},1}
{A} is non empty trivial V36() V40() 1 -element V44() V45() V46() V47() V48() V49() Element of bool {{},1}
bool {{},1} is non empty V36() V40() set
{{},1} \ {A} is V36() V40() V44() V45() V46() V47() V48() V49() Element of bool {{},1}
{1} is non empty trivial V36() V40() 1 -element V44() V45() V46() V47() V48() V49() Element of bool K168()
bool K168() is non empty non trivial V36() set
{{},1} \ {1} is V36() V40() V44() V45() V46() V47() V48() V49() Element of bool {{},1}
{{}} is non empty trivial V36() V40() 1 -element V44() V45() V46() V47() V48() V49() set
{{},1} \ {{}} is V36() V40() V44() V45() V46() V47() V48() V49() Element of bool {{},1}
A is V26() V31() V35() V36() cardinal Element of {{},1}
{A} is non empty trivial V36() V40() 1 -element V44() V45() V46() V47() V48() V49() Element of bool {{},1}
bool {{},1} is non empty V36() V40() set
{{},1} \ {A} is V36() V40() V44() V45() V46() V47() V48() V49() Element of bool {{},1}
F is non empty non trivial set
[:F,F:] is non empty set
[:[:F,F:],F:] is non empty set
bool [:[:F,F:],F:] is non empty set
F is set
bool F is non empty set
[:F,F:] is set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
A is Element of bool F
[:A,A:] is set
pr1 (F,F) is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) Element of bool [:[:F,F:],F:]
y is set
(pr1 (F,F)) . y is set
p is set
q is set
[p,q] is non empty set
(pr1 (F,F)) . (p,q) is set
(pr1 (F,F)) . [p,q] is set
y is set
(pr1 (F,F)) . y is set
F is set
bool F is non empty set
[:F,F:] is set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
A is Element of bool F
[:A,A:] is set
F is set
bool F is non empty set
[:F,F:] is set
A is Element of bool F
[:A,A:] is set
[:[:A,A:],A:] is set
bool [:[:A,A:],A:] is non empty set
F is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) (F,A)
(F,A) is Relation-like Function-like set
F | [:A,A:] is Relation-like Function-like set
dom F is Relation-like set
dom (F,A) is set
y is set
(F,A) . y is set
F . y is set
F is set
bool F is non empty set
[:F,F:] is set
A is Element of bool F
F is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) (F,A)
(F,A) is Relation-like Function-like set
[:A,A:] is set
F | [:A,A:] is Relation-like Function-like set
[:[:A,A:],A:] is set
bool [:[:A,A:],A:] is non empty set
F is set
[:F,F:] is set
[:[:F,F:],F:] is set
bool [:[:F,F:],F:] is non empty set
A is Element of F
{A} is non empty trivial V36() 1 -element set
F \ {A} is Element of bool F
bool F is non empty set
[:(F \ {A}),(F \ {A}):] is set
F is non empty non trivial set
[:F,F:] is non empty set
A is Element of F
{A} is non empty trivial V36() 1 -element Element of bool F
bool F is non empty set
F \ {A} is Element of bool F
[:(F \ {A}),(F \ {A}):] is set
[:[:(F \ {A}),(F \ {A}):],(F \ {A}):] is set
bool [:[:(F \ {A}),(F \ {A}):],(F \ {A}):] is non empty set
F is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) (F,A)
(F,(F \ {A})) is Relation-like Function-like set
F | [:(F \ {A}),(F \ {A}):] is Relation-like Function-like set
dom F is Relation-like set
dom (F,(F \ {A})) is set
y is set
(F,(F \ {A})) . y is set
F . y is set
F is non empty non trivial set
[:F,F:] is non empty set
A is Element of F
F is Relation-like [:F,F:] -defined F -valued Function-like V18([:F,F:],F) (F,A)
{A} is non empty trivial V36() 1 -element Element of bool F
bool F is non empty set
F \ {A} is Element of bool F
(F,(F \ {A})) is Relation-like Function-like set
[:(F \ {A}),(F \ {A}):] is set
F | [:(F \ {A}),(F \ {A}):] is Relation-like Function-like set
[:[:(F \ {A}),(F \ {A}):],(F \ {A}):] is set
bool [:[:(F \ {A}),(F \ {A}):],(F \ {A}):] is non empty set
F is non empty non trivial set
bool F is non empty set
A is non empty trivial V36() 1 -element Element of bool F
F \ A is Element of bool F
F is Element of F
{F} is non empty trivial V36() 1 -element Element of bool F
F is non empty non trivial set
bool F is non empty set
A is non empty trivial V36() 1 -element Element of bool F
F \ A is Element of bool F