:: DOMAIN_1 semantic presentation

{} is empty V7() V8() V9() set
the empty V7() V8() V9() set is empty V7() V8() V9() set
A is set
a is non empty set
B is non empty set
[:a,B:] is non empty V7() set
x is set
y is set
[x,y] is V1() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
x6 is Element of a
x5 is Element of B
[x6,x5] is V1() set
{x6,x5} is non empty set
{x6} is non empty set
{{x6,x5},{x6}} is non empty set
A is non empty set
a is non empty set
[:A,a:] is non empty V7() set
B is Element of [:A,a:]
B `1 is set
x is Element of [:A,a:]
x `1 is set
B `2 is set
x `2 is set
[(B `1),(B `2)] is V1() set
{(B `1),(B `2)} is non empty set
{(B `1)} is non empty set
{{(B `1),(B `2)},{(B `1)}} is non empty set
A is non empty set
a is non empty set
B is Element of A
x is Element of a
[B,x] is V1() set
{B,x} is non empty set
{B} is non empty set
{{B,x},{B}} is non empty set
[:A,a:] is non empty V7() set
A is non empty set
a is non empty set
[:A,a:] is non empty V7() set
B is Element of [:A,a:]
B `1 is set
B `2 is set
A is set
a is non empty set
B is non empty set
x is non empty set
[:a,B,x:] is non empty set
[:a,B:] is non empty V7() set
[:[:a,B:],x:] is non empty V7() set
y is set
x5 is set
[y,x5] is V1() set
{y,x5} is non empty set
{y} is non empty set
{{y,x5},{y}} is non empty set
x7 is set
x8 is set
[x7,x8] is V1() set
{x7,x8} is non empty set
{x7} is non empty set
{{x7,x8},{x7}} is non empty set
A2 is Element of a
A1 is Element of B
x6 is Element of x
[A2,A1,x6] is V1() V2() set
[A2,A1] is V1() set
{A2,A1} is non empty set
{A2} is non empty set
{{A2,A1},{A2}} is non empty set
[[A2,A1],x6] is V1() set
{[A2,A1],x6} is non empty set
{[A2,A1]} is non empty V7() set
{{[A2,A1],x6},{[A2,A1]}} is non empty set
y is Element of a
x5 is Element of B
x6 is Element of x
[y,x5,x6] is V1() V2() set
[y,x5] is V1() set
{y,x5} is non empty set
{y} is non empty set
{{y,x5},{y}} is non empty set
[[y,x5],x6] is V1() set
{[y,x5],x6} is non empty set
{[y,x5]} is non empty V7() set
{{[y,x5],x6},{[y,x5]}} is non empty set
[:a,B:] is non empty V7() set
(a,B,y,x5) is V1() Element of [:a,B:]
([:a,B:],x,(a,B,y,x5),x6) is V1() Element of [:[:a,B:],x:]
[:[:a,B:],x:] is non empty V7() set
{(a,B,y,x5),x6} is non empty set
{(a,B,y,x5)} is non empty V7() set
{{(a,B,y,x5),x6},{(a,B,y,x5)}} is non empty set
A is non empty set
a is non empty set
B is non empty set
x is non empty set
[:a,B,x:] is non empty set
y is set
[:a,B:] is non empty V7() set
[:[:a,B:],x:] is non empty V7() set
x5 is Element of a
x6 is Element of B
x7 is Element of x
[x5,x6,x7] is V1() V2() set
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
[[x5,x6],x7] is V1() set
{[x5,x6],x7} is non empty set
{[x5,x6]} is non empty V7() set
{{[x5,x6],x7},{[x5,x6]}} is non empty set
(a,B,x5,x6) is V1() Element of [:a,B:]
([:a,B:],x,(a,B,x5,x6),x7) is V1() Element of [:[:a,B:],x:]
{(a,B,x5,x6),x7} is non empty set
{(a,B,x5,x6)} is non empty V7() set
{{(a,B,x5,x6),x7},{(a,B,x5,x6)}} is non empty set
x5 is set
x6 is set
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
x8 is set
A1 is set
[x8,A1] is V1() set
{x8,A1} is non empty set
{x8} is non empty set
{{x8,A1},{x8}} is non empty set
A3 is Element of a
A2 is Element of B
x7 is Element of x
[A3,A2,x7] is V1() V2() set
[A3,A2] is V1() set
{A3,A2} is non empty set
{A3} is non empty set
{{A3,A2},{A3}} is non empty set
[[A3,A2],x7] is V1() set
{[A3,A2],x7} is non empty set
{[A3,A2]} is non empty V7() set
{{[A3,A2],x7},{[A3,A2]}} is non empty set
a is non empty set
B is non empty set
x is non empty set
A is non empty set
[:a,B,x:] is non empty set
y is set
x5 is set
x6 is Element of a
x7 is Element of B
x8 is Element of x
[x6,x7,x8] is V1() V2() set
[x6,x7] is V1() set
{x6,x7} is non empty set
{x6} is non empty set
{{x6,x7},{x6}} is non empty set
[[x6,x7],x8] is V1() set
{[x6,x7],x8} is non empty set
{[x6,x7]} is non empty V7() set
{{[x6,x7],x8},{[x6,x7]}} is non empty set
A1 is non empty set
A2 is non empty set
A3 is non empty set
A4 is non empty set
[:A2,A3,A4:] is non empty set
A is non empty set
a is non empty set
B is non empty set
x is Element of A
y is Element of a
x5 is Element of B
[x,y,x5] is V1() V2() set
[x,y] is V1() set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[[x,y],x5] is V1() set
{[x,y],x5} is non empty set
{[x,y]} is non empty V7() set
{{[x,y],x5},{[x,y]}} is non empty set
[:A,a,B:] is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
[:a,B,x:] is non empty set
y is V1() V2() Element of [:a,B,x:]
y `1_3 is Element of a
y `1 is set
(y `1) `1 is set
y `2_3 is Element of B
(y `1) `2 is set
y `3_3 is Element of x
(a,B,x,(y `1_3),(y `2_3),(y `3_3)) is V1() V2() Element of [:a,B,x:]
[(y `1_3),(y `2_3)] is V1() set
{(y `1_3),(y `2_3)} is non empty set
{(y `1_3)} is non empty set
{{(y `1_3),(y `2_3)},{(y `1_3)}} is non empty set
[[(y `1_3),(y `2_3)],(y `3_3)] is V1() set
{[(y `1_3),(y `2_3)],(y `3_3)} is non empty set
{[(y `1_3),(y `2_3)]} is non empty V7() set
{{[(y `1_3),(y `2_3)],(y `3_3)},{[(y `1_3),(y `2_3)]}} is non empty set
x5 is Element of a
x6 is Element of B
x7 is Element of x
(a,B,x,x5,x6,x7) is V1() V2() Element of [:a,B,x:]
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
[[x5,x6],x7] is V1() set
{[x5,x6],x7} is non empty set
{[x5,x6]} is non empty V7() set
{{[x5,x6],x7},{[x5,x6]}} is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
[:a,B,x:] is non empty set
y is V1() V2() Element of [:a,B,x:]
y `2_3 is Element of B
y `1 is set
(y `1) `2 is set
y `1_3 is Element of a
(y `1) `1 is set
y `3_3 is Element of x
(a,B,x,(y `1_3),(y `2_3),(y `3_3)) is V1() V2() Element of [:a,B,x:]
[(y `1_3),(y `2_3)] is V1() set
{(y `1_3),(y `2_3)} is non empty set
{(y `1_3)} is non empty set
{{(y `1_3),(y `2_3)},{(y `1_3)}} is non empty set
[[(y `1_3),(y `2_3)],(y `3_3)] is V1() set
{[(y `1_3),(y `2_3)],(y `3_3)} is non empty set
{[(y `1_3),(y `2_3)]} is non empty V7() set
{{[(y `1_3),(y `2_3)],(y `3_3)},{[(y `1_3),(y `2_3)]}} is non empty set
x5 is Element of a
x6 is Element of B
x7 is Element of x
(a,B,x,x5,x6,x7) is V1() V2() Element of [:a,B,x:]
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
[[x5,x6],x7] is V1() set
{[x5,x6],x7} is non empty set
{[x5,x6]} is non empty V7() set
{{[x5,x6],x7},{[x5,x6]}} is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
[:a,B,x:] is non empty set
y is V1() V2() Element of [:a,B,x:]
y `3_3 is Element of x
y `1_3 is Element of a
y `1 is set
(y `1) `1 is set
y `2_3 is Element of B
(y `1) `2 is set
(a,B,x,(y `1_3),(y `2_3),(y `3_3)) is V1() V2() Element of [:a,B,x:]
[(y `1_3),(y `2_3)] is V1() set
{(y `1_3),(y `2_3)} is non empty set
{(y `1_3)} is non empty set
{{(y `1_3),(y `2_3)},{(y `1_3)}} is non empty set
[[(y `1_3),(y `2_3)],(y `3_3)] is V1() set
{[(y `1_3),(y `2_3)],(y `3_3)} is non empty set
{[(y `1_3),(y `2_3)]} is non empty V7() set
{{[(y `1_3),(y `2_3)],(y `3_3)},{[(y `1_3),(y `2_3)]}} is non empty set
x5 is Element of a
x6 is Element of B
x7 is Element of x
(a,B,x,x5,x6,x7) is V1() V2() Element of [:a,B,x:]
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
[[x5,x6],x7] is V1() set
{[x5,x6],x7} is non empty set
{[x5,x6]} is non empty V7() set
{{[x5,x6],x7},{[x5,x6]}} is non empty set
A is non empty set
a is non empty set
B is non empty set
[:A,a,B:] is non empty set
x is V1() V2() Element of [:A,a,B:]
x `1_3 is Element of A
x `1 is set
(x `1) `1 is set
x `2_3 is Element of a
(x `1) `2 is set
x `3_3 is Element of B
y is V1() V2() Element of [:A,a,B:]
y `1_3 is Element of A
y `1 is set
(y `1) `1 is set
y `2_3 is Element of a
(y `1) `2 is set
y `3_3 is Element of B
(A,a,B,(x `1_3),(x `2_3),(x `3_3)) is V1() V2() Element of [:A,a,B:]
[(x `1_3),(x `2_3)] is V1() set
{(x `1_3),(x `2_3)} is non empty set
{(x `1_3)} is non empty set
{{(x `1_3),(x `2_3)},{(x `1_3)}} is non empty set
[[(x `1_3),(x `2_3)],(x `3_3)] is V1() set
{[(x `1_3),(x `2_3)],(x `3_3)} is non empty set
{[(x `1_3),(x `2_3)]} is non empty V7() set
{{[(x `1_3),(x `2_3)],(x `3_3)},{[(x `1_3),(x `2_3)]}} is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
y is non empty set
[:a,B,x,y:] is non empty set
[:a,B,x:] is non empty set
[:[:a,B,x:],y:] is non empty V7() set
x5 is set
x6 is set
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
x8 is Element of a
A1 is Element of B
A2 is Element of x
(a,B,x,x8,A1,A2) is V1() V2() Element of [:a,B,x:]
[x8,A1] is V1() set
{x8,A1} is non empty set
{x8} is non empty set
{{x8,A1},{x8}} is non empty set
[[x8,A1],A2] is V1() set
{[x8,A1],A2} is non empty set
{[x8,A1]} is non empty V7() set
{{[x8,A1],A2},{[x8,A1]}} is non empty set
x7 is Element of y
[x8,A1,A2,x7] is V1() V2() V3() set
[x8,A1,A2] is V1() V2() set
[[x8,A1,A2],x7] is V1() set
{[x8,A1,A2],x7} is non empty set
{[x8,A1,A2]} is non empty set
{{[x8,A1,A2],x7},{[x8,A1,A2]}} is non empty set
x5 is Element of a
x6 is Element of B
x7 is Element of x
x8 is Element of y
[x5,x6,x7,x8] is V1() V2() V3() set
[x5,x6,x7] is V1() V2() set
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
[[x5,x6],x7] is V1() set
{[x5,x6],x7} is non empty set
{[x5,x6]} is non empty V7() set
{{[x5,x6],x7},{[x5,x6]}} is non empty set
[[x5,x6,x7],x8] is V1() set
{[x5,x6,x7],x8} is non empty set
{[x5,x6,x7]} is non empty set
{{[x5,x6,x7],x8},{[x5,x6,x7]}} is non empty set
[:a,B,x:] is non empty set
(a,B,x,x5,x6,x7) is V1() V2() Element of [:a,B,x:]
([:a,B,x:],y,(a,B,x,x5,x6,x7),x8) is V1() Element of [:[:a,B,x:],y:]
[:[:a,B,x:],y:] is non empty V7() set
{(a,B,x,x5,x6,x7),x8} is non empty set
{(a,B,x,x5,x6,x7)} is non empty set
{{(a,B,x,x5,x6,x7),x8},{(a,B,x,x5,x6,x7)}} is non empty set
A is non empty set
a is non empty set
B is non empty set
x is non empty set
y is non empty set
[:a,B,x,y:] is non empty set
x5 is set
[:a,B,x:] is non empty set
[:[:a,B,x:],y:] is non empty V7() set
x6 is Element of a
x7 is Element of B
x8 is Element of x
A1 is Element of y
[x6,x7,x8,A1] is V1() V2() V3() set
[x6,x7,x8] is V1() V2() set
[x6,x7] is V1() set
{x6,x7} is non empty set
{x6} is non empty set
{{x6,x7},{x6}} is non empty set
[[x6,x7],x8] is V1() set
{[x6,x7],x8} is non empty set
{[x6,x7]} is non empty V7() set
{{[x6,x7],x8},{[x6,x7]}} is non empty set
[[x6,x7,x8],A1] is V1() set
{[x6,x7,x8],A1} is non empty set
{[x6,x7,x8]} is non empty set
{{[x6,x7,x8],A1},{[x6,x7,x8]}} is non empty set
(a,B,x,x6,x7,x8) is V1() V2() Element of [:a,B,x:]
([:a,B,x:],y,(a,B,x,x6,x7,x8),A1) is V1() Element of [:[:a,B,x:],y:]
{(a,B,x,x6,x7,x8),A1} is non empty set
{(a,B,x,x6,x7,x8)} is non empty set
{{(a,B,x,x6,x7,x8),A1},{(a,B,x,x6,x7,x8)}} is non empty set
x6 is set
x7 is set
[x6,x7] is V1() set
{x6,x7} is non empty set
{x6} is non empty set
{{x6,x7},{x6}} is non empty set
A1 is Element of a
A2 is Element of B
A3 is Element of x
(a,B,x,A1,A2,A3) is V1() V2() Element of [:a,B,x:]
[A1,A2] is V1() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
[[A1,A2],A3] is V1() set
{[A1,A2],A3} is non empty set
{[A1,A2]} is non empty V7() set
{{[A1,A2],A3},{[A1,A2]}} is non empty set
x8 is Element of y
[A1,A2,A3,x8] is V1() V2() V3() set
[A1,A2,A3] is V1() V2() set
[[A1,A2,A3],x8] is V1() set
{[A1,A2,A3],x8} is non empty set
{[A1,A2,A3]} is non empty set
{{[A1,A2,A3],x8},{[A1,A2,A3]}} is non empty set
a is non empty set
B is non empty set
x is non empty set
y is non empty set
A is non empty set
[:a,B,x,y:] is non empty set
x5 is set
x6 is set
x7 is Element of a
x8 is Element of B
A1 is Element of x
A2 is Element of y
[x7,x8,A1,A2] is V1() V2() V3() set
[x7,x8,A1] is V1() V2() set
[x7,x8] is V1() set
{x7,x8} is non empty set
{x7} is non empty set
{{x7,x8},{x7}} is non empty set
[[x7,x8],A1] is V1() set
{[x7,x8],A1} is non empty set
{[x7,x8]} is non empty V7() set
{{[x7,x8],A1},{[x7,x8]}} is non empty set
[[x7,x8,A1],A2] is V1() set
{[x7,x8,A1],A2} is non empty set
{[x7,x8,A1]} is non empty set
{{[x7,x8,A1],A2},{[x7,x8,A1]}} is non empty set
A3 is non empty set
A4 is non empty set
x is non empty set
c₁₅ is non empty set
c₁₆ is non empty set
[:A4,x,c₁₅,c₁₆:] is non empty set
A is non empty set
a is non empty set
B is non empty set
x is non empty set
y is Element of A
x5 is Element of a
x6 is Element of B
x7 is Element of x
[y,x5,x6,x7] is V1() V2() V3() set
[y,x5,x6] is V1() V2() set
[y,x5] is V1() set
{y,x5} is non empty set
{y} is non empty set
{{y,x5},{y}} is non empty set
[[y,x5],x6] is V1() set
{[y,x5],x6} is non empty set
{[y,x5]} is non empty V7() set
{{[y,x5],x6},{[y,x5]}} is non empty set
[[y,x5,x6],x7] is V1() set
{[y,x5,x6],x7} is non empty set
{[y,x5,x6]} is non empty set
{{[y,x5,x6],x7},{[y,x5,x6]}} is non empty set
[:A,a,B,x:] is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
y is non empty set
[:a,B,x,y:] is non empty set
x5 is V1() V2() V3() Element of [:a,B,x,y:]
x5 `1_4 is Element of a
x5 `1 is set
(x5 `1) `1 is set
((x5 `1) `1) `1 is set
x5 `2_4 is Element of B
((x5 `1) `1) `2 is set
x5 `3_4 is Element of x
(x5 `1) `2 is set
x5 `4_4 is Element of y
(a,B,x,y,(x5 `1_4),(x5 `2_4),(x5 `3_4),(x5 `4_4)) is V1() V2() V3() Element of [:a,B,x,y:]
[(x5 `1_4),(x5 `2_4),(x5 `3_4)] is V1() V2() set
[(x5 `1_4),(x5 `2_4)] is V1() set
{(x5 `1_4),(x5 `2_4)} is non empty set
{(x5 `1_4)} is non empty set
{{(x5 `1_4),(x5 `2_4)},{(x5 `1_4)}} is non empty set
[[(x5 `1_4),(x5 `2_4)],(x5 `3_4)] is V1() set
{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)} is non empty set
{[(x5 `1_4),(x5 `2_4)]} is non empty V7() set
{{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)},{[(x5 `1_4),(x5 `2_4)]}} is non empty set
[[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)] is V1() set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)} is non empty set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]} is non empty set
{{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)},{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]}} is non empty set
x6 is Element of a
x7 is Element of B
x8 is Element of x
A1 is Element of y
(a,B,x,y,x6,x7,x8,A1) is V1() V2() V3() Element of [:a,B,x,y:]
[x6,x7,x8] is V1() V2() set
[x6,x7] is V1() set
{x6,x7} is non empty set
{x6} is non empty set
{{x6,x7},{x6}} is non empty set
[[x6,x7],x8] is V1() set
{[x6,x7],x8} is non empty set
{[x6,x7]} is non empty V7() set
{{[x6,x7],x8},{[x6,x7]}} is non empty set
[[x6,x7,x8],A1] is V1() set
{[x6,x7,x8],A1} is non empty set
{[x6,x7,x8]} is non empty set
{{[x6,x7,x8],A1},{[x6,x7,x8]}} is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
y is non empty set
[:a,B,x,y:] is non empty set
x5 is V1() V2() V3() Element of [:a,B,x,y:]
x5 `2_4 is Element of B
x5 `1 is set
(x5 `1) `1 is set
((x5 `1) `1) `2 is set
x5 `1_4 is Element of a
((x5 `1) `1) `1 is set
x5 `3_4 is Element of x
(x5 `1) `2 is set
x5 `4_4 is Element of y
(a,B,x,y,(x5 `1_4),(x5 `2_4),(x5 `3_4),(x5 `4_4)) is V1() V2() V3() Element of [:a,B,x,y:]
[(x5 `1_4),(x5 `2_4),(x5 `3_4)] is V1() V2() set
[(x5 `1_4),(x5 `2_4)] is V1() set
{(x5 `1_4),(x5 `2_4)} is non empty set
{(x5 `1_4)} is non empty set
{{(x5 `1_4),(x5 `2_4)},{(x5 `1_4)}} is non empty set
[[(x5 `1_4),(x5 `2_4)],(x5 `3_4)] is V1() set
{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)} is non empty set
{[(x5 `1_4),(x5 `2_4)]} is non empty V7() set
{{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)},{[(x5 `1_4),(x5 `2_4)]}} is non empty set
[[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)] is V1() set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)} is non empty set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]} is non empty set
{{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)},{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]}} is non empty set
x6 is Element of a
x7 is Element of B
x8 is Element of x
A1 is Element of y
(a,B,x,y,x6,x7,x8,A1) is V1() V2() V3() Element of [:a,B,x,y:]
[x6,x7,x8] is V1() V2() set
[x6,x7] is V1() set
{x6,x7} is non empty set
{x6} is non empty set
{{x6,x7},{x6}} is non empty set
[[x6,x7],x8] is V1() set
{[x6,x7],x8} is non empty set
{[x6,x7]} is non empty V7() set
{{[x6,x7],x8},{[x6,x7]}} is non empty set
[[x6,x7,x8],A1] is V1() set
{[x6,x7,x8],A1} is non empty set
{[x6,x7,x8]} is non empty set
{{[x6,x7,x8],A1},{[x6,x7,x8]}} is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
y is non empty set
[:a,B,x,y:] is non empty set
x5 is V1() V2() V3() Element of [:a,B,x,y:]
x5 `3_4 is Element of x
x5 `1 is set
(x5 `1) `2 is set
x5 `1_4 is Element of a
(x5 `1) `1 is set
((x5 `1) `1) `1 is set
x5 `2_4 is Element of B
((x5 `1) `1) `2 is set
x5 `4_4 is Element of y
(a,B,x,y,(x5 `1_4),(x5 `2_4),(x5 `3_4),(x5 `4_4)) is V1() V2() V3() Element of [:a,B,x,y:]
[(x5 `1_4),(x5 `2_4),(x5 `3_4)] is V1() V2() set
[(x5 `1_4),(x5 `2_4)] is V1() set
{(x5 `1_4),(x5 `2_4)} is non empty set
{(x5 `1_4)} is non empty set
{{(x5 `1_4),(x5 `2_4)},{(x5 `1_4)}} is non empty set
[[(x5 `1_4),(x5 `2_4)],(x5 `3_4)] is V1() set
{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)} is non empty set
{[(x5 `1_4),(x5 `2_4)]} is non empty V7() set
{{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)},{[(x5 `1_4),(x5 `2_4)]}} is non empty set
[[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)] is V1() set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)} is non empty set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]} is non empty set
{{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)},{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]}} is non empty set
x6 is Element of a
x7 is Element of B
x8 is Element of x
A1 is Element of y
(a,B,x,y,x6,x7,x8,A1) is V1() V2() V3() Element of [:a,B,x,y:]
[x6,x7,x8] is V1() V2() set
[x6,x7] is V1() set
{x6,x7} is non empty set
{x6} is non empty set
{{x6,x7},{x6}} is non empty set
[[x6,x7],x8] is V1() set
{[x6,x7],x8} is non empty set
{[x6,x7]} is non empty V7() set
{{[x6,x7],x8},{[x6,x7]}} is non empty set
[[x6,x7,x8],A1] is V1() set
{[x6,x7,x8],A1} is non empty set
{[x6,x7,x8]} is non empty set
{{[x6,x7,x8],A1},{[x6,x7,x8]}} is non empty set
A is set
a is non empty set
B is non empty set
x is non empty set
y is non empty set
[:a,B,x,y:] is non empty set
x5 is V1() V2() V3() Element of [:a,B,x,y:]
x5 `4_4 is Element of y
x5 `1_4 is Element of a
x5 `1 is set
(x5 `1) `1 is set
((x5 `1) `1) `1 is set
x5 `2_4 is Element of B
((x5 `1) `1) `2 is set
x5 `3_4 is Element of x
(x5 `1) `2 is set
(a,B,x,y,(x5 `1_4),(x5 `2_4),(x5 `3_4),(x5 `4_4)) is V1() V2() V3() Element of [:a,B,x,y:]
[(x5 `1_4),(x5 `2_4),(x5 `3_4)] is V1() V2() set
[(x5 `1_4),(x5 `2_4)] is V1() set
{(x5 `1_4),(x5 `2_4)} is non empty set
{(x5 `1_4)} is non empty set
{{(x5 `1_4),(x5 `2_4)},{(x5 `1_4)}} is non empty set
[[(x5 `1_4),(x5 `2_4)],(x5 `3_4)] is V1() set
{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)} is non empty set
{[(x5 `1_4),(x5 `2_4)]} is non empty V7() set
{{[(x5 `1_4),(x5 `2_4)],(x5 `3_4)},{[(x5 `1_4),(x5 `2_4)]}} is non empty set
[[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)] is V1() set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)} is non empty set
{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]} is non empty set
{{[(x5 `1_4),(x5 `2_4),(x5 `3_4)],(x5 `4_4)},{[(x5 `1_4),(x5 `2_4),(x5 `3_4)]}} is non empty set
x6 is Element of a
x7 is Element of B
x8 is Element of x
A1 is Element of y
(a,B,x,y,x6,x7,x8,A1) is V1() V2() V3() Element of [:a,B,x,y:]
[x6,x7,x8] is V1() V2() set
[x6,x7] is V1() set
{x6,x7} is non empty set
{x6} is non empty set
{{x6,x7},{x6}} is non empty set
[[x6,x7],x8] is V1() set
{[x6,x7],x8} is non empty set
{[x6,x7]} is non empty V7() set
{{[x6,x7],x8},{[x6,x7]}} is non empty set
[[x6,x7,x8],A1] is V1() set
{[x6,x7,x8],A1} is non empty set
{[x6,x7,x8]} is non empty set
{{[x6,x7,x8],A1},{[x6,x7,x8]}} is non empty set
A is non empty set
a is non empty set
B is non empty set
x is non empty set
[:A,a,B,x:] is non empty set
y is V1() V2() V3() Element of [:A,a,B,x:]
y `1_4 is Element of A
y `1 is set
(y `1) `1 is set
((y `1) `1) `1 is set
x5 is V1() V2() V3() Element of [:A,a,B,x:]
x5 `1_4 is Element of A
x5 `1 is set
(x5 `1) `1 is set
((x5 `1) `1) `1 is set
y `2_4 is Element of a
((y `1) `1) `2 is set
x5 `2_4 is Element of a
((x5 `1) `1) `2 is set
y `3_4 is Element of B
(y `1) `2 is set
x5 `3_4 is Element of B
(x5 `1) `2 is set
y `4_4 is Element of x
x5 `4_4 is Element of x
(A,a,B,x,(y `1_4),(y `2_4),(y `3_4),(y `4_4)) is V1() V2() V3() Element of [:A,a,B,x:]
[(y `1_4),(y `2_4),(y `3_4)] is V1() V2() set
[(y `1_4),(y `2_4)] is V1() set
{(y `1_4),(y `2_4)} is non empty set
{(y `1_4)} is non empty set
{{(y `1_4),(y `2_4)},{(y `1_4)}} is non empty set
[[(y `1_4),(y `2_4)],(y `3_4)] is V1() set
{[(y `1_4),(y `2_4)],(y `3_4)} is non empty set
{[(y `1_4),(y `2_4)]} is non empty V7() set
{{[(y `1_4),(y `2_4)],(y `3_4)},{[(y `1_4),(y `2_4)]}} is non empty set
[[(y `1_4),(y `2_4),(y `3_4)],(y `4_4)] is V1() set
{[(y `1_4),(y `2_4),(y `3_4)],(y `4_4)} is non empty set
{[(y `1_4),(y `2_4),(y `3_4)]} is non empty set
{{[(y `1_4),(y `2_4),(y `3_4)],(y `4_4)},{[(y `1_4),(y `2_4),(y `3_4)]}} is non empty set
A is non empty set
{ b₁ where b₁ is Element of A : P₁[b₁] } is set
bool A is non empty set
a is set
B is Element of A
A is non empty set
a is non empty set
{ (A,a,b₁,b₂) where b₁ is Element of A, b₂ is Element of a : P₁[b₁,b₂] } is set
[:A,a:] is non empty V7() set
bool [:A,a:] is non empty set
B is set
x is Element of A
y is Element of a
(A,a,x,y) is V1() Element of [:A,a:]
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
A is non empty set
a is non empty set
B is non empty set
{ (A,a,B,b₁,b₂,b₃) where b₁ is Element of A, b₂ is Element of a, b₃ is Element of B : P₁[b₁,b₂,b₃] } is set
[:A,a,B:] is non empty set
bool [:A,a,B:] is non empty set
x is set
y is Element of A
x5 is Element of a
x6 is Element of B
(A,a,B,y,x5,x6) is V1() V2() Element of [:A,a,B:]
[y,x5] is V1() set
{y,x5} is non empty set
{y} is non empty set
{{y,x5},{y}} is non empty set
[[y,x5],x6] is V1() set
{[y,x5],x6} is non empty set
{[y,x5]} is non empty V7() set
{{[y,x5],x6},{[y,x5]}} is non empty set
A is non empty set
a is non empty set
B is non empty set
x is non empty set
{ (A,a,B,x,b₁,b₂,b₃,b₄) where b₁ is Element of A, b₂ is Element of a, b₃ is Element of B, b₄ is Element of x : P₁[b₁,b₂,b₃,b₄] } is set
[:A,a,B,x:] is non empty set
bool [:A,a,B,x:] is non empty set
y is set
x5 is Element of A
x6 is Element of a
x7 is Element of B
x8 is Element of x
(A,a,B,x,x5,x6,x7,x8) is V1() V2() V3() Element of [:A,a,B,x:]
[x5,x6,x7] is V1() V2() set
[x5,x6] is V1() set
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
[[x5,x6],x7] is V1() set
{[x5,x6],x7} is non empty set
{[x5,x6]} is non empty V7() set
{{[x5,x6],x7},{[x5,x6]}} is non empty set
[[x5,x6,x7],x8] is V1() set
{[x5,x6,x7],x8} is non empty set
{[x5,x6,x7]} is non empty set
{{[x5,x6,x7],x8},{[x5,x6,x7]}} is non empty set
A is non empty set
{ b₁ where b₁ is Element of A : P₁[b₁] } is set
{ b₁ where b₁ is Element of A : P₂[b₁] } is set
a is set
B is Element of A
A is non empty set
{ b₁ where b₁ is Element of A : P₁[b₁] } is set
{ b₁ where b₁ is Element of A : P₂[b₁] } is set
F₁() is non empty set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
bool F₁() is non empty set
A is non empty set
{ b₁ where b₁ is Element of A : verum } is set
a is Element of A
{ b₁ where b₁ is Element of A : S₁[b₁] } is set
bool A is non empty set
A is non empty set
a is non empty set
[:A,a:] is non empty V7() set
{ (A,a,b₁,b₂) where b₁ is Element of A, b₂ is Element of a : verum } is set
B is Element of [:A,a:]
(A,a,B) is Element of A
(A,a,B) is Element of a
(A,a,(A,a,B),(A,a,B)) is V1() Element of [:A,a:]
{(A,a,B),(A,a,B)} is non empty set
{(A,a,B)} is non empty set
{{(A,a,B),(A,a,B)},{(A,a,B)}} is non empty set
bool [:A,a:] is non empty set
A is non empty set
a is non empty set
B is non empty set
[:A,a,B:] is non empty set
{ (A,a,B,b₁,b₂,b₃) where b₁ is Element of A, b₂ is Element of a, b₃ is Element of B : verum } is set
x is V1() V2() Element of [:A,a,B:]
x `1_3 is Element of A
x `1 is set
(x `1) `1 is set
x `2_3 is Element of a
(x `1) `2 is set
x `3_3 is Element of B
(A,a,B,(x `1_3),(x `2_3),(x `3_3)) is V1() V2() Element of [:A,a,B:]
[(x `1_3),(x `2_3)] is V1() set
{(x `1_3),(x `2_3)} is non empty set
{(x `1_3)} is non empty set
{{(x `1_3),(x `2_3)},{(x `1_3)}} is non empty set
[[(x `1_3),(x `2_3)],(x `3_3)] is V1() set
{[(x `1_3),(x `2_3)],(x `3_3)} is non empty set
{[(x `1_3),(x `2_3)]} is non empty V7() set
{{[(x `1_3),(x `2_3)],(x `3_3)},{[(x `1_3),(x `2_3)]}} is non empty set
bool [:A,a,B:] is non empty set
A is non empty set
a is non empty set
B is non empty set
x is non empty set
[:A,a,B,x:] is non empty set
{ (A,a,B,x,b₁,b₂,b₃,b₄) where b₁ is Element of A, b₂ is Element of a, b₃ is Element of B, b₄ is Element of x : verum } is set
y is V1() V2() V3() Element of [:A,a,B,x:]
y `1_4 is Element of A
y `1 is set
(y `1) `1 is set
((y `1) `1) `1 is set
y `2_4 is Element of a
((y `1) `1) `2 is set
y `3_4 is Element of B
(y `1) `2 is set
y `4_4 is Element of x
(A,a,B,x,(y `1_4),(y `2_4),(y `3_4),(y `4_4)) is V1() V2() V3() Element of [:A,a,B,x:]
[(y `1_4),(y `2_4),(y `3_4)] is V1() V2() set
[(y `1_4),(y `2_4)] is V1() set
{(y `1_4),(y `2_4)} is non empty set
{(y `1_4)} is non empty set
{{(y `1_4),(y `2_4)},{(y `1_4)}} is non empty set
[[(y `1_4),(y `2_4)],(y `3_4)] is V1() set
{[(y `1_4),(y `2_4)],(y `3_4)} is non empty set
{[(y `1_4),(y `2_4)]} is non empty V7() set
{{[(y `1_4),(y `2_4)],(y `3_4)},{[(y `1_4),(y `2_4)]}} is non empty set
[[(y `1_4),(y `2_4),(y `3_4)],(y `4_4)] is V1() set
{[(y `1_4),(y `2_4),(y `3_4)],(y `4_4)} is non empty set
{[(y `1_4),(y `2_4),(y `3_4)]} is non empty set
{{[(y `1_4),(y `2_4),(y `3_4)],(y `4_4)},{[(y `1_4),(y `2_4),(y `3_4)]}} is non empty set
bool [:A,a,B,x:] is non empty set
A is non empty set
bool A is non empty set
a is Element of bool A
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : b<sub>1</sub> in a } is set
B is set
B is set
x is Element of A
A is non empty set
bool A is non empty set
a is non empty set
bool a is non empty set
B is Element of bool A
x is Element of bool a
[:B,x:] is V7() Element of bool [:A,a:]
[:A,a:] is non empty V7() set
bool [:A,a:] is non empty set
{ (A,a,b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub> is Element of A, b<sub>2</sub> is Element of a : ( b<sub>1</sub> in B & b<sub>2</sub> in x ) } is set
y is set
x5 is Element of [:A,a:]
(A,a,x5) is Element of A
(A,a,x5) is Element of a
(A,a,(A,a,x5),(A,a,x5)) is V1() Element of [:A,a:]
{(A,a,x5),(A,a,x5)} is non empty set
{(A,a,x5)} is non empty set
{{(A,a,x5),(A,a,x5)},{(A,a,x5)}} is non empty set
y is set
x5 is Element of A
x6 is Element of a
(A,a,x5,x6) is V1() Element of [:A,a:]
{x5,x6} is non empty set
{x5} is non empty set
{{x5,x6},{x5}} is non empty set
A is non empty set
bool A is non empty set
a is non empty set
bool a is non empty set
B is non empty set
bool B is non empty set
x is Element of bool A
y is Element of bool a
x5 is Element of bool B
[:x,y,x5:] is Element of bool [:A,a,B:]
[:A,a,B:] is non empty set
bool [:A,a,B:] is non empty set
{ (A,a,B,b<sub>1</sub>,b<sub>2</sub>,b<sub>3</sub>) where b<sub>1</sub> is Element of A, b<sub>2</sub> is Element of a, b<sub>3</sub> is Element of B : ( b<sub>1</sub> in x & b<sub>2</sub> in y & b<sub>3</sub> in x5 ) } is set
x6 is set
x7 is non empty Element of bool A
x8 is non empty Element of bool a
A1 is non empty Element of bool B
[:x7,x8,A1:] is non empty Element of bool [:A,a,B:]
A2 is V1() V2() Element of [:A,a,B:]
A2 `1_3 is Element of A
A2 `1 is set
(A2 `1) `1 is set
A2 `2_3 is Element of a
(A2 `1) `2 is set
A2 `3_3 is Element of B
(A,a,B,(A2 `1_3),(A2 `2_3),(A2 `3_3)) is V1() V2() Element of [:A,a,B:]
[(A2 `1_3),(A2 `2_3)] is V1() set
{(A2 `1_3),(A2 `2_3)} is non empty set
{(A2 `1_3)} is non empty set
{{(A2 `1_3),(A2 `2_3)},{(A2 `1_3)}} is non empty set
[[(A2 `1_3),(A2 `2_3)],(A2 `3_3)] is V1() set
{[(A2 `1_3),(A2 `2_3)],(A2 `3_3)} is non empty set
{[(A2 `1_3),(A2 `2_3)]} is non empty V7() set
{{[(A2 `1_3),(A2 `2_3)],(A2 `3_3)},{[(A2 `1_3),(A2 `2_3)]}} is non empty set
x6 is set
x7 is Element of A
x8 is Element of a
A1 is Element of B
(A,a,B,x7,x8,A1) is V1() V2() Element of [:A,a,B:]
[x7,x8] is V1() set
{x7,x8} is non empty set
{x7} is non empty set
{{x7,x8},{x7}} is non empty set
[[x7,x8],A1] is V1() set
{[x7,x8],A1} is non empty set
{[x7,x8]} is non empty V7() set
{{[x7,x8],A1},{[x7,x8]}} is non empty set
A is non empty set
bool A is non empty set
a is non empty set
bool a is non empty set
B is non empty set
bool B is non empty set
x is non empty set
bool x is non empty set
y is Element of bool A
x5 is Element of bool a
x6 is Element of bool B
x7 is Element of bool x
[:y,x5,x6,x7:] is Element of bool [:A,a,B,x:]
[:A,a,B,x:] is non empty set
bool [:A,a,B,x:] is non empty set
{ (A,a,B,x,b<sub>1</sub>,b<sub>2</sub>,b<sub>3</sub>,b<sub>4</sub>) where b<sub>1</sub> is Element of A, b<sub>2</sub> is Element of a, b<sub>3</sub> is Element of B, b<sub>4</sub> is Element of x : ( b<sub>1</sub> in y & b<sub>2</sub> in x5 & b<sub>3</sub> in x6 & b<sub>4</sub> in x7 ) } is set
x8 is set
A1 is non empty Element of bool A
A2 is non empty Element of bool a
A3 is non empty Element of bool B
A4 is non empty Element of bool x
[:A1,A2,A3,A4:] is non empty Element of bool [:A,a,B,x:]
x is V1() V2() V3() Element of [:A,a,B,x:]
x `3_4 is Element of B
x `1 is set
(x `1) `2 is set
x `4_4 is Element of x
x `1_4 is Element of A
(x `1) `1 is set
((x `1) `1) `1 is set
x `2_4 is Element of a
((x `1) `1) `2 is set
(A,a,B,x,(x `1_4),(x `2_4),(x `3_4),(x `4_4)) is V1() V2() V3() Element of [:A,a,B,x:]
[(x `1_4),(x `2_4),(x `3_4)] is V1() V2() set
[(x `1_4),(x `2_4)] is V1() set
{(x `1_4),(x `2_4)} is non empty set
{(x `1_4)} is non empty set
{{(x `1_4),(x `2_4)},{(x `1_4)}} is non empty set
[[(x `1_4),(x `2_4)],(x `3_4)] is V1() set
{[(x `1_4),(x `2_4)],(x `3_4)} is non empty set
{[(x `1_4),(x `2_4)]} is non empty V7() set
{{[(x `1_4),(x `2_4)],(x `3_4)},{[(x `1_4),(x `2_4)]}} is non empty set
[[(x `1_4),(x `2_4),(x `3_4)],(x `4_4)] is V1() set
{[(x `1_4),(x `2_4),(x `3_4)],(x `4_4)} is non empty set
{[(x `1_4),(x `2_4),(x `3_4)]} is non empty set
{{[(x `1_4),(x `2_4),(x `3_4)],(x `4_4)},{[(x `1_4),(x `2_4),(x `3_4)]}} is non empty set
x8 is set
A1 is Element of A
A2 is Element of a
A3 is Element of B
A4 is Element of x
(A,a,B,x,A1,A2,A3,A4) is V1() V2() V3() Element of [:A,a,B,x:]
[A1,A2,A3] is V1() V2() set
[A1,A2] is V1() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
[[A1,A2],A3] is V1() set
{[A1,A2],A3} is non empty set
{[A1,A2]} is non empty V7() set
{{[A1,A2],A3},{[A1,A2]}} is non empty set
[[A1,A2,A3],A4] is V1() set
{[A1,A2,A3],A4} is non empty set
{[A1,A2,A3]} is non empty set
{{[A1,A2,A3],A4},{[A1,A2,A3]}} is non empty set
A is non empty set
{} A is empty proper V7() V8() V9() Element of bool A
bool A is non empty set
{ b₁ where b₁ is Element of A : contradiction } is set
a is set
a is set
B is Element of A
A is non empty set
bool A is non empty set
a is Element of bool A
a ` is Element of bool A
A \ a is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : not b<sub>1</sub> in a } is set
B is set
B is set
x is Element of A
A is non empty set
bool A is non empty set
a is Element of bool A
B is Element of bool A
a /\ B is Element of bool A
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( b<sub>1</sub> in a & b<sub>1</sub> in B ) } is set
x is set
y is Element of A
x is set
y is Element of A
A is non empty set
bool A is non empty set
a is Element of bool A
B is Element of bool A
a \/ B is Element of bool A
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( b<sub>1</sub> in a or b<sub>1</sub> in B ) } is set
x is set
y is Element of A
x is set
y is Element of A
A is non empty set
bool A is non empty set
a is Element of bool A
B is Element of bool A
a \ B is Element of bool A
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( b<sub>1</sub> in a & not b<sub>1</sub> in B ) } is set
x is set
y is Element of A
x is set
y is Element of A
A is non empty set
bool A is non empty set
a is Element of bool A
B is Element of bool A
a \+\ B is Element of bool A
a \ B is set
B \ a is set
(a \ B) \/ (B \ a) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( ( b<sub>1</sub> in a & not b<sub>1</sub> in B ) or ( not b<sub>1</sub> in a & b<sub>1</sub> in B ) ) } is set
x is set
y is Element of A
x is set
y is Element of A
A is non empty set
bool A is non empty set
a is Element of bool A
B is Element of bool A
a \+\ B is Element of bool A
a \ B is set
B \ a is set
(a \ B) \/ (B \ a) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( ( b<sub>1</sub> in a or b<sub>1</sub> in B ) & ( not b<sub>1</sub> in B or not b<sub>1</sub> in a ) ) } is set
x is Element of A
y is Element of A
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( ( b<sub>1</sub> in a & not b<sub>1</sub> in B ) or ( not b<sub>1</sub> in a & b<sub>1</sub> in B ) ) } is set
A is non empty set
bool A is non empty set
a is Element of bool A
B is Element of bool A
a \+\ B is Element of bool A
a \ B is set
B \ a is set
(a \ B) \/ (B \ a) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( ( not b<sub>1</sub> in a or not b<sub>1</sub> in B ) & ( b<sub>1</sub> in B or b<sub>1</sub> in a ) ) } is set
x is Element of A
y is Element of A
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( ( b<sub>1</sub> in a or b<sub>1</sub> in B ) & ( not b<sub>1</sub> in B or not b<sub>1</sub> in a ) ) } is set
A is non empty set
bool A is non empty set
a is Element of bool A
B is Element of bool A
a \+\ B is Element of bool A
a \ B is set
B \ a is set
(a \ B) \/ (B \ a) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( ( b<sub>1</sub> in a & not b<sub>1</sub> in B ) or ( b<sub>1</sub> in B & not b<sub>1</sub> in a ) ) } is set
x is Element of A
y is Element of A
{ b<sub>1</sub> where b<sub>1</sub> is Element of A : ( ( b<sub>1</sub> in a or b<sub>1</sub> in B ) & ( not b<sub>1</sub> in B or not b<sub>1</sub> in a ) ) } is set
A is non empty set
a is Element of A
{a} is non empty set
bool A is non empty set
B is Element of A
{a,B} is non empty set
x is Element of A
{a,B,x} is non empty set
y is Element of A
{a,B,x,y} is non empty set
x5 is Element of A
{a,B,x,y,x5} is non empty set
x6 is Element of A
{a,B,x,y,x5,x6} is non empty set
x7 is Element of A
{a,B,x,y,x5,x6,x7} is non empty set
x8 is Element of A
{a,B,x,y,x5,x6,x7,x8} is non empty set
F<sub>2</sub>() is non empty set
F<sub>1</sub>() is non empty set
{ F<sub>3</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of F<sub>1</sub>() : P<sub>1</sub>[b<sub>1</sub>] } is set
bool F<sub>2</sub>() is non empty set
a is set
B is Element of F<sub>1</sub>()
F<sub>3</sub>(B) is Element of F<sub>2</sub>()
F<sub>3</sub>() is non empty set
F<sub>1</sub>() is non empty set
F<sub>2</sub>() is non empty set
{ F<sub>4</sub>(b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub> is Element of F<sub>1</sub>(), b<sub>2</sub> is Element of F<sub>2</sub>() : P<sub>1</sub>[b<sub>1</sub>,b<sub>2</sub>] } is set
bool F<sub>3</sub>() is non empty set
a is set
B is Element of F<sub>1</sub>()
x is Element of F<sub>2</sub>()
F<sub>4</sub>(B,x) is Element of F<sub>3</sub>()
A is non empty set
a is non empty set
[:A,a:] is non empty V7() set
B is non empty set
[:[:A,a:],B:] is non empty V7() set
x is Element of [:[:A,a:],B:]
x `11 is set
([:A,a:],B,x) is Element of [:A,a:]
(A,a,([:A,a:],B,x)) is Element of A
x `12 is set
([:A,a:],B,x) is Element of [:A,a:]
(A,a,([:A,a:],B,x)) is Element of a
A is non empty set
a is non empty set
B is non empty set
[:a,B:] is non empty V7() set
[:A,[:a,B:]:] is non empty V7() set
x is Element of [:A,[:a,B:]:]
x `21 is set
(A,[:a,B:],x) is Element of [:a,B:]
(a,B,(A,[:a,B:],x)) is Element of a
x `22 is set
(A,[:a,B:],x) is Element of [:a,B:]
(a,B,(A,[:a,B:],x)) is Element of B
F₁() is non empty set
{ b₁ where b₁ is Element of F₁() : ( P₁[b₁] & P₂[b₁] ) } is set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
{ b₁ where b₁ is Element of F₁() : P₂[b₁] } is set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } /\ { b₁ where b₁ is Element of F₁() : P₂[b₁] } is set
x is set
y is Element of F₁()
x is set
y is Element of F₁()
x5 is Element of F₁()
A is non empty set
bool A is non empty set
the Element of A is Element of A
(A, the Element of A) is non empty Element of bool A
B is non empty Element of bool A
x is set
y is set