:: REALSET1 semantic presentation

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