:: COMBGRAS semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty non trivial non finite set

[:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V27() V28() ext-real non positive non negative finite V57() cardinal {} -element set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V27() V28() ext-real non positive non negative finite V57() cardinal {} -element Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

card {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V27() V28() ext-real non positive non negative finite V57() cardinal {} -element set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is set

F is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

card F is epsilon-transitive epsilon-connected ordinal cardinal set

X /\ F is set

card (X /\ F) is epsilon-transitive epsilon-connected ordinal cardinal set

X \/ F is set

card (X \/ F) is epsilon-transitive epsilon-connected ordinal cardinal set

succ k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + X is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

2 * X is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + (2 * X) is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

F is set

card F is epsilon-transitive epsilon-connected ordinal cardinal set

s is set

card s is epsilon-transitive epsilon-connected ordinal cardinal set

F /\ s is set

card (F /\ s) is epsilon-transitive epsilon-connected ordinal cardinal set

F \/ s is set

card (F \/ s) is epsilon-transitive epsilon-connected ordinal cardinal set

(k + X) + (k + X) is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

((k + X) + (k + X)) - k is V27() V28() ext-real Element of REAL

(k + X) + (k + X) is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

A is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal set

((k + X) + (k + X)) - A is V27() V28() ext-real Element of REAL

k is set

card k is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

F is Relation-like Function-like set

dom F is set

rng F is set

F .: k is set

F is Relation-like Function-like set

dom F is set

F .: k is set

F | k is Relation-like Function-like set

rng (F | k) is set

s is set

dom (F | k) is set

A is set

(F | k) . A is set

F . A is set

dom (F | k) is set

k is set

card k is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like Function-like set

dom X is set

X .: k is set

card (X .: k) is epsilon-transitive epsilon-connected ordinal cardinal set

k is set

X is set

k \ X is Element of bool k

bool k is non empty set

F is set

k \ F is Element of bool k

F \/ k is set

X \ F is Element of bool X

bool X is non empty set

X \/ k is set

F \ X is Element of bool F

bool F is non empty set

k is set

bool k is non empty set

X is non empty set

[:k,X:] is set

bool [:k,X:] is non empty set

F is Relation-like k -defined X -valued Function-like V32(k) quasi_total Element of bool [:k,X:]

s is Element of bool k

F .: s is set

A is Element of bool k

F .: A is set

dom F is Element of bool k

L is set

F . L is set

X2 is set

F . X2 is set

L is set

F . L is set

X2 is set

F . X2 is set

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k - 1 is V27() V28() ext-real Element of REAL

k - 2 is V27() V28() ext-real Element of REAL

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

k - 3 is V27() V28() ext-real Element of REAL

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

F is set

card F is epsilon-transitive epsilon-connected ordinal cardinal set

s is set

card s is epsilon-transitive epsilon-connected ordinal cardinal set

X /\ F is set

card (X /\ F) is epsilon-transitive epsilon-connected ordinal cardinal set

X /\ s is set

card (X /\ s) is epsilon-transitive epsilon-connected ordinal cardinal set

F /\ s is set

card (F /\ s) is epsilon-transitive epsilon-connected ordinal cardinal set

(X /\ F) /\ s is set

card ((X /\ F) /\ s) is epsilon-transitive epsilon-connected ordinal cardinal set

X \/ F is set

(X \/ F) \/ s is set

card ((X \/ F) \/ s) is epsilon-transitive epsilon-connected ordinal cardinal set

2 - 1 is V27() V28() ext-real Element of REAL

(k + 1) - 1 is V27() V28() ext-real Element of REAL

X \ (X /\ F) is Element of bool X

bool X is non empty set

card (X \ (X /\ F)) is epsilon-transitive epsilon-connected ordinal cardinal set

(k - 1) - (k - 2) is V27() V28() ext-real Element of REAL

A is set

{A} is non empty trivial finite 1 -element set

F \ (X /\ F) is Element of bool F

bool F is non empty set

card (F \ (X /\ F)) is epsilon-transitive epsilon-connected ordinal cardinal set

L is set

{L} is non empty trivial finite 1 -element set

s \ (X /\ s) is Element of bool s

bool s is non empty set

card (s \ (X /\ s)) is epsilon-transitive epsilon-connected ordinal cardinal set

X2 is set

{X2} is non empty trivial finite 1 -element set

(X /\ F) \/ {A} is non empty set

(F /\ s) /\ X is set

(X /\ s) /\ F is set

(X /\ F) \/ {L} is non empty set

(X /\ s) \/ {X2} is non empty set

((X /\ F) /\ s) /\ {A} is finite set

B1 is set

(X /\ s) \ {A} is Element of bool (X /\ s)

bool (X /\ s) is non empty set

B1 is set

{A,L} is non empty finite set

(X /\ F) /\ {A,L} is finite set

B1 is set

{A} \/ {L} is non empty finite set

(X /\ F) \/ ({A} \/ {L}) is non empty set

(X /\ F) \/ {A,L} is non empty set

card {A} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega

card ((X /\ s) \ {A}) is epsilon-transitive epsilon-connected ordinal cardinal set

(k - 2) - 1 is V27() V28() ext-real Element of REAL

B1 is set

- 2 is V27() V28() ext-real non positive Element of REAL

(- 2) + k is V27() V28() ext-real Element of REAL

- 3 is V27() V28() ext-real non positive Element of REAL

(- 3) + k is V27() V28() ext-real Element of REAL

card {A,L} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega

card (X \/ F) is epsilon-transitive epsilon-connected ordinal cardinal set

(k - 2) + 2 is V27() V28() ext-real Element of REAL

X \ {A} is Element of bool X

card (X \ {A}) is epsilon-transitive epsilon-connected ordinal cardinal set

(k - 1) - 1 is V27() V28() ext-real Element of REAL

(X /\ s) /\ {A} is finite set

(X /\ F) /\ {A} is finite set

B1 is set

{A,L,X2} is non empty finite set

(X /\ F) /\ {A,L,X2} is finite set

B1 is set

{A} \/ {L} is non empty finite set

(X /\ F) \/ ({A} \/ {L}) is non empty set

{A,L} is non empty finite set

(X /\ F) \/ {A,L} is non empty set

{A,L} \/ {X2} is non empty finite set

(X /\ F) \/ ({A,L} \/ {X2}) is non empty set

(X /\ F) \/ {A,L,X2} is non empty set

(X /\ F) /\ (X /\ s) is set

F /\ X is set

(F /\ X) /\ X is set

((F /\ X) /\ X) /\ s is set

X /\ X is set

F /\ (X /\ X) is set

(F /\ (X /\ X)) /\ s is set

card {A,L,X2} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega

(k - 2) + 3 is V27() V28() ext-real Element of REAL

{A,L} is non empty finite set

{A,L} \/ {X2} is non empty finite set

((X /\ F) /\ s) \/ ({A,L} \/ {X2}) is non empty set

{A,L,X2} is non empty finite set

((X /\ F) /\ s) \/ {A,L,X2} is non empty set

k is IncProjStr

the Points of k is non empty set

the Lines of k is non empty set

the Inc of k is Relation-like the Points of k -defined the Lines of k -valued Element of bool [: the Points of k, the Lines of k:]

[: the Points of k, the Lines of k:] is non empty set

bool [: the Points of k, the Lines of k:] is non empty set

IncProjStr(# the Points of k, the Lines of k, the Inc of k #) is strict IncProjStr

X is IncProjStr

the Points of X is non empty set

the Lines of X is non empty set

the Inc of X is Relation-like the Points of X -defined the Lines of X -valued Element of bool [: the Points of X, the Lines of X:]

[: the Points of X, the Lines of X:] is non empty set

bool [: the Points of X, the Lines of X:] is non empty set

IncProjStr(# the Points of X, the Lines of X, the Inc of X #) is strict IncProjStr

F is Element of the Points of k

s is Element of the Points of X

A is Element of the Lines of k

L is Element of the Lines of X

[s,L] is Element of [: the Points of X, the Lines of X:]

{s,L} is non empty finite set

{s} is non empty trivial finite 1 -element set

{{s,L},{s}} is non empty finite V57() set

k is IncProjStr

the Points of k is non empty set

the Lines of k is non empty set

the Inc of k is Relation-like the Points of k -defined the Lines of k -valued Element of bool [: the Points of k, the Lines of k:]

[: the Points of k, the Lines of k:] is non empty set

bool [: the Points of k, the Lines of k:] is non empty set

IncProjStr(# the Points of k, the Lines of k, the Inc of k #) is strict IncProjStr

X is IncProjStr

the Points of X is non empty set

the Lines of X is non empty set

the Inc of X is Relation-like the Points of X -defined the Lines of X -valued Element of bool [: the Points of X, the Lines of X:]

[: the Points of X, the Lines of X:] is non empty set

bool [: the Points of X, the Lines of X:] is non empty set

IncProjStr(# the Points of X, the Lines of X, the Inc of X #) is strict IncProjStr

bool the Points of k is non empty set

bool the Points of X is non empty set

F is Element of bool the Points of k

s is Element of bool the Points of X

A is Element of the Lines of k

L is Element of the Lines of X

X2 is Element of the Points of X

B1 is Element of the Points of k

[X2,L] is Element of [: the Points of X, the Lines of X:]

{X2,L} is non empty finite set

{X2} is non empty trivial finite 1 -element set

{{X2,L},{X2}} is non empty finite V57() set

the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct is strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct is non empty set

the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct is non empty set

the Inc of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct is Relation-like the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct -defined the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct -valued Element of bool [: the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct , the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct :]

[: the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct , the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct :] is non empty set

bool [: the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct , the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct :] is non empty set

IncProjStr(# the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct , the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct , the Inc of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct #) is strict IncProjStr

X is strict IncProjStr

the Lines of X is non empty set

the Points of X is non empty set

F is Element of the Lines of X

s is Element of the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

A is Element of the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

L is Element of the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

{A,L} is non empty finite Element of bool the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

bool the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct is non empty set

X2 is Element of the Points of X

B1 is Element of the Points of X

{X2,B1} is non empty finite Element of bool the Points of X

bool the Points of X is non empty set

F is Element of the Points of X

s is Element of the Points of X

A is Element of the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

L is Element of the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

{A,L} is non empty finite Element of bool the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

bool the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct is non empty set

X2 is Element of the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

B1 is Element of the Lines of X

F is Element of the Points of X

s is Element of the Points of X

{F,s} is non empty finite Element of bool the Points of X

bool the Points of X is non empty set

A is Element of the Lines of X

L is Element of the Lines of X

b1 is Element of the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

C1 is Element of the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

{b1,C1} is non empty finite Element of bool the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

bool the Points of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct is non empty set

X2 is Element of the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

B1 is Element of the Lines of the strict with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncStruct

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is non empty set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

bool X is non empty set

{ b

{ b

bool X is non empty Element of bool (bool X)

bool (bool X) is non empty set

RelIncl (bool X) is Relation-like set

[: { b

(RelIncl (bool X)) /\ [: { b

L is set

card L is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is set

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

b1 is non empty set

X2 is non empty set

[:b1,X2:] is non empty set

bool [:b1,X2:] is non empty set

C1 is Relation-like b1 -defined X2 -valued Element of bool [:b1,X2:]

IncProjStr(# b1,X2,C1 #) is strict IncProjStr

the Points of IncProjStr(# b1,X2,C1 #) is non empty set

the Lines of IncProjStr(# b1,X2,C1 #) is non empty set

a1 is Element of the Points of IncProjStr(# b1,X2,C1 #)

S is Element of the Points of IncProjStr(# b1,X2,C1 #)

{a1,S} is non empty finite Element of bool the Points of IncProjStr(# b1,X2,C1 #)

bool the Points of IncProjStr(# b1,X2,C1 #) is non empty set

ha1 is Element of the Lines of IncProjStr(# b1,X2,C1 #)

ha1 is Element of the Lines of IncProjStr(# b1,X2,C1 #)

a1 \/ S is set

card (a1 \/ S) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is Element of bool X

card A2 is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

[S,ha1] is Element of [: the Points of IncProjStr(# b1,X2,C1 #), the Lines of IncProjStr(# b1,X2,C1 #):]

[: the Points of IncProjStr(# b1,X2,C1 #), the Lines of IncProjStr(# b1,X2,C1 #):] is non empty set

{S,ha1} is non empty finite set

{S} is non empty trivial finite 1 -element set

{{S,ha1},{S}} is non empty finite V57() set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is Element of bool X

card A2 is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

[a1,ha1] is Element of [: the Points of IncProjStr(# b1,X2,C1 #), the Lines of IncProjStr(# b1,X2,C1 #):]

{a1,ha1} is non empty finite set

{a1} is non empty trivial finite 1 -element set

{{a1,ha1},{a1}} is non empty finite V57() set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is Element of bool X

card A2 is epsilon-transitive epsilon-connected ordinal cardinal set

[S,ha1] is Element of [: the Points of IncProjStr(# b1,X2,C1 #), the Lines of IncProjStr(# b1,X2,C1 #):]

{S,ha1} is non empty finite set

{{S,ha1},{S}} is non empty finite V57() set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is Element of bool X

card A2 is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

[a1,ha1] is Element of [: the Points of IncProjStr(# b1,X2,C1 #), the Lines of IncProjStr(# b1,X2,C1 #):]

{a1,ha1} is non empty finite set

{{a1,ha1},{a1}} is non empty finite V57() set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is Element of bool X

card A2 is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

the Lines of IncProjStr(# b1,X2,C1 #) is non empty set

the Points of IncProjStr(# b1,X2,C1 #) is non empty set

a1 is Element of the Lines of IncProjStr(# b1,X2,C1 #)

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

ha1 is set

ha1 is set

{ha1} is non empty trivial finite 1 -element set

S \ {ha1} is Element of bool X

{ha1} is non empty trivial finite 1 -element set

S \ {ha1} is Element of bool X

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is Element of bool X

card A2 is epsilon-transitive epsilon-connected ordinal cardinal set

y2 is Element of the Points of IncProjStr(# b1,X2,C1 #)

A1 is Element of the Points of IncProjStr(# b1,X2,C1 #)

{y2,A1} is non empty finite Element of bool the Points of IncProjStr(# b1,X2,C1 #)

bool the Points of IncProjStr(# b1,X2,C1 #) is non empty set

{ha1} \/ S is non empty set

{ha1} \/ S is non empty set

B2 is Element of the Points of IncProjStr(# b1,X2,C1 #)

[B2,a1] is Element of [: the Points of IncProjStr(# b1,X2,C1 #), the Lines of IncProjStr(# b1,X2,C1 #):]

[: the Points of IncProjStr(# b1,X2,C1 #), the Lines of IncProjStr(# b1,X2,C1 #):] is non empty set

{B2,a1} is non empty finite set

{B2} is non empty trivial finite 1 -element set

{{B2,a1},{B2}} is non empty finite V57() set

F is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of F is non empty set

the Lines of F is non empty set

the Inc of F is Relation-like the Points of F -defined the Lines of F -valued Element of bool [: the Points of F, the Lines of F:]

[: the Points of F, the Lines of F:] is non empty set

bool [: the Points of F, the Lines of F:] is non empty set

(RelIncl (bool X)) /\ [: the Points of F, the Lines of F:] is set

s is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of s is non empty set

the Lines of s is non empty set

the Inc of s is Relation-like the Points of s -defined the Lines of s -valued Element of bool [: the Points of s, the Lines of s:]

[: the Points of s, the Lines of s:] is non empty set

bool [: the Points of s, the Lines of s:] is non empty set

(RelIncl (bool X)) /\ [: the Points of s, the Lines of s:] is set

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is non empty set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of (k,X) is non empty set

the Lines of (k,X) is non empty set

bool X is non empty set

{ b

F is Element of the Points of (k,X)

{ b

s is Element of the Lines of (k,X)

the Inc of (k,X) is Relation-like the Points of (k,X) -defined the Lines of (k,X) -valued Element of bool [: the Points of (k,X), the Lines of (k,X):]

[: the Points of (k,X), the Lines of (k,X):] is non empty set

bool [: the Points of (k,X), the Lines of (k,X):] is non empty set

bool X is non empty Element of bool (bool X)

bool (bool X) is non empty set

RelIncl (bool X) is Relation-like set

(RelIncl (bool X)) /\ [: the Points of (k,X), the Lines of (k,X):] is set

[F,s] is Element of [: the Points of (k,X), the Lines of (k,X):]

{F,s} is non empty finite set

{F} is non empty trivial finite 1 -element set

{{F,s},{F}} is non empty finite V57() set

A is Element of bool X

card A is epsilon-transitive epsilon-connected ordinal cardinal set

L is Element of bool X

card L is epsilon-transitive epsilon-connected ordinal cardinal set

[F,s] is Element of [: the Points of (k,X), the Lines of (k,X):]

{F,s} is non empty finite set

{F} is non empty trivial finite 1 -element set

{{F,s},{F}} is non empty finite V57() set

A is Element of bool X

card A is epsilon-transitive epsilon-connected ordinal cardinal set

L is Element of bool X

card L is epsilon-transitive epsilon-connected ordinal cardinal set

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is non empty set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of (k,X) is non empty set

bool X is non empty set

{ b

the Lines of (k,X) is non empty set

F is Element of the Points of (k,X)

s is Element of the Points of (k,X)

A is Element of the Points of (k,X)

L is Element of the Points of (k,X)

X2 is Element of the Points of (k,X)

b1 is Element of the Lines of (k,X)

C1 is Element of the Lines of (k,X)

b2 is Element of the Lines of (k,X)

a1 is Element of the Lines of (k,X)

{F,X2} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

{s,X2} is non empty finite Element of bool the Points of (k,X)

{ b

b1 /\ C1 is set

card (b1 /\ C1) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

F \/ A is set

card (F \/ A) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

s \/ L is set

card (s \/ L) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

b1 \/ C1 is set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

succ k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

card (b1 \/ C1) is epsilon-transitive epsilon-connected ordinal cardinal set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + (2 * 1) is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

b2 \/ a1 is set

card (b2 \/ a1) is epsilon-transitive epsilon-connected ordinal cardinal set

k + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

succ (k + 2) is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

(k + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

succ (k + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

2 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V27() V28() ext-real non positive non negative finite V57() cardinal {} -element Element of NAT

(k + 1) + (2 * 0) is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

b2 /\ a1 is set

card (b2 /\ a1) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

S is set

card S is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

ha1 is Element of the Points of (k,X)

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is non empty set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of (k,X) is non empty set

the Lines of (k,X) is non empty set

bool X is non empty set

{ b

{ b

F is Element of the Points of (k,X)

s is Element of the Points of (k,X)

A is Element of the Points of (k,X)

L is Element of the Points of (k,X)

X2 is Element of the Points of (k,X)

F /\ s is set

A /\ L is set

(F /\ s) \/ (A /\ L) is set

b1 is Element of the Lines of (k,X)

C1 is Element of the Lines of (k,X)

b2 is Element of the Lines of (k,X)

a1 is Element of the Lines of (k,X)

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

k - 1 is V27() V28() ext-real Element of REAL

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

b2 /\ a1 is set

card (b2 /\ a1) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

succ k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of the Points of (k,X)

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

F \/ s is set

card (F \/ s) is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

A \/ L is set

card (A \/ L) is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

(k - 1) + 1 is V27() V28() ext-real Element of REAL

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

card ((F /\ s) \/ (A /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

succ (k - 1) is non empty set

card F is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

{F,S} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

{A,S} is non empty finite Element of bool the Points of (k,X)

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

(k - 1) + (2 * 1) is V27() V28() ext-real Element of REAL

card (F /\ s) is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

card (A /\ L) is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

b1 /\ C1 is set

(F /\ s) /\ (A /\ L) is set

(F /\ s) /\ A is set

((F /\ s) /\ A) /\ L is set

F \ (((F /\ s) /\ A) /\ L) is Element of bool F

bool F is non empty set

(((F /\ s) /\ A) /\ L) \/ (F \ (((F /\ s) /\ A) /\ L)) is set

2 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V27() V28() ext-real non positive non negative finite V57() cardinal {} -element Element of NAT

(k - 1) + (2 * 0) is V27() V28() ext-real Element of REAL

card ((F /\ s) /\ (A /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

card (F \ (((F /\ s) /\ A) /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

k - (k - 1) is V27() V28() ext-real Element of REAL

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is set

{ha1} is non empty trivial finite 1 -element set

s \ (((F /\ s) /\ A) /\ L) is Element of bool s

bool s is non empty set

(((F /\ s) /\ A) /\ L) \/ (s \ (((F /\ s) /\ A) /\ L)) is set

card (s \ (((F /\ s) /\ A) /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is set

{ha1} is non empty trivial finite 1 -element set

L \ (((F /\ s) /\ A) /\ L) is Element of bool L

bool L is non empty set

(((F /\ s) /\ A) /\ L) \/ (L \ (((F /\ s) /\ A) /\ L)) is set

card (L \ (((F /\ s) /\ A) /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

S is set

{S} is non empty trivial finite 1 -element set

A \ (((F /\ s) /\ A) /\ L) is Element of bool A

bool A is non empty set

(((F /\ s) /\ A) /\ L) \/ (A \ (((F /\ s) /\ A) /\ L)) is set

card (A \ (((F /\ s) /\ A) /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is Element of bool X

card A2 is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is set

{A2} is non empty trivial finite 1 -element set

y2 is Element of bool X

card y2 is epsilon-transitive epsilon-connected ordinal cardinal set

A1 is Element of bool X

card A1 is epsilon-transitive epsilon-connected ordinal cardinal set

B2 is Element of bool X

card B2 is epsilon-transitive epsilon-connected ordinal cardinal set

y2 is Element of bool X

card y2 is epsilon-transitive epsilon-connected ordinal cardinal set

{A2} \/ {S} is non empty finite set

(((F /\ s) /\ A) /\ L) \/ ({A2} \/ {S}) is non empty set

{A2,S} is non empty finite set

(((F /\ s) /\ A) /\ L) \/ {A2,S} is non empty set

{F,X2} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

{s,X2} is non empty finite Element of bool the Points of (k,X)

y2 is Element of bool X

card y2 is epsilon-transitive epsilon-connected ordinal cardinal set

A1 is Element of bool X

card A1 is epsilon-transitive epsilon-connected ordinal cardinal set

B2 is Element of bool X

card B2 is epsilon-transitive epsilon-connected ordinal cardinal set

y2 is Element of bool X

card y2 is epsilon-transitive epsilon-connected ordinal cardinal set

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

(((F /\ s) /\ A) /\ L) \/ ({ha1} \/ {ha1}) is non empty set

{ha1,ha1} is non empty finite set

(((F /\ s) /\ A) /\ L) \/ {ha1,ha1} is non empty set

y2 is set

card k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega

card (k - 1) is epsilon-transitive epsilon-connected ordinal cardinal set

y2 is Element of bool X

card y2 is epsilon-transitive epsilon-connected ordinal cardinal set

ha1 is Element of bool X

card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set

{L,S} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

{A,S} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

{F,S} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

{s,S} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is non empty set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of (k,X) is non empty set

the Lines of (k,X) is non empty set

F is Element of the Points of (k,X)

s is Element of the Points of (k,X)

A is Element of the Points of (k,X)

{F,s,A} is non empty finite Element of bool the Points of (k,X)

bool the Points of (k,X) is non empty set

X2 is Element of the Points of (k,X)

L is Element of the Points of (k,X)

{F,X2,L} is non empty finite Element of bool the Points of (k,X)

b1 is Element of the Points of (k,X)

B1 is Element of the Points of (k,X)

{F,b1,B1} is non empty finite Element of bool the Points of (k,X)

a1 is Element of the Points of (k,X)

{b1,X2,a1} is non empty finite Element of bool the Points of (k,X)

C1 is Element of the Points of (k,X)

{b1,C1,A} is non empty finite Element of bool the Points of (k,X)

b2 is Element of the Points of (k,X)

{X2,b2,A} is non empty finite Element of bool the Points of (k,X)

{a1,L,B1} is non empty finite Element of bool the Points of (k,X)

{s,C1,B1} is non empty finite Element of bool the Points of (k,X)

{s,b2,L} is non empty finite Element of bool the Points of (k,X)

{C1,b2,a1} is non empty finite Element of bool the Points of (k,X)

S is Element of the Lines of (k,X)

ha1 is Element of the Lines of (k,X)

ha1 is Element of the Lines of (k,X)

S is Element of the Lines of (k,X)

A2 is Element of the Lines of (k,X)

y2 is Element of the Lines of (k,X)

A1 is Element of the Lines of (k,X)

B2 is Element of the Lines of (k,X)

a2 is Element of the Lines of (k,X)

{X2,L} is non empty finite Element of bool the Points of (k,X)

{F,L} is non empty finite Element of bool the Points of (k,X)

{F,X2} is non empty finite Element of bool the Points of (k,X)

{b1,B1} is non empty finite Element of bool the Points of (k,X)

{F,B1} is non empty finite Element of bool the Points of (k,X)

{F,b1} is non empty finite Element of bool the Points of (k,X)

{F,s} is non empty finite Element of bool the Points of (k,X)

{A,s} is non empty finite Element of bool the Points of (k,X)

bool X is non empty set

{ b

{F,A} is non empty finite Element of bool the Points of (k,X)

A /\ s is set

X2 /\ L is set

(A /\ s) \/ (X2 /\ L) is set

A2 is Element of the Points of (k,X)

b1 /\ B1 is set

(A /\ s) \/ (b1 /\ B1) is set

L3a is Element of the Points of (k,X)

((A /\ s) \/ (b1 /\ B1)) \/ (X2 /\ L) is set

(b1 /\ B1) \/ (X2 /\ L) is set

(A /\ s) \/ ((b1 /\ B1) \/ (X2 /\ L)) is set

(X2 /\ L) \/ (b1 /\ B1) is set

L3b is Element of the Points of (k,X)

{b2,A2} is non empty finite Element of bool the Points of (k,X)

{C1,L3a} is non empty finite Element of bool the Points of (k,X)

{a1,L3b} is non empty finite Element of bool the Points of (k,X)

C1 \/ b2 is set

(b1 /\ B1) \/ (A /\ s) is set

((b1 /\ B1) \/ (A /\ s)) \/ (A /\ s) is set

(((b1 /\ B1) \/ (A /\ s)) \/ (A /\ s)) \/ (X2 /\ L) is set

(A /\ s) \/ (A /\ s) is set

(b1 /\ B1) \/ ((A /\ s) \/ (A /\ s)) is set

((b1 /\ B1) \/ ((A /\ s) \/ (A /\ s))) \/ (X2 /\ L) is set

(C1 \/ b2) \/ a1 is set

X2 \/ L is set

b2 \/ a1 is set

C1 \/ (b2 \/ a1) is set

A \/ s is set

card (A \/ s) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

{ b

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

k - 1 is V27() V28() ext-real Element of REAL

(k - 1) + 1 is V27() V28() ext-real Element of REAL

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

K11 is Element of bool X

card K11 is epsilon-transitive epsilon-connected ordinal cardinal set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

(k - 1) + (2 * 1) is V27() V28() ext-real Element of REAL

card (X2 \/ L) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

K11 is Element of bool X

card K11 is epsilon-transitive epsilon-connected ordinal cardinal set

card (X2 /\ L) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

k - 2 is V27() V28() ext-real Element of REAL

(k - 2) + 1 is V27() V28() ext-real Element of REAL

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

card (A /\ s) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

b1 \/ B1 is set

C1 \/ a1 is set

b2 \/ (C1 \/ a1) is set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is set

{D} is non empty trivial finite 1 -element set

K11 is Element of bool X

card K11 is epsilon-transitive epsilon-connected ordinal cardinal set

K11 is set

{K11} is non empty trivial finite 1 -element set

K13 is Element of bool X

card K13 is epsilon-transitive epsilon-connected ordinal cardinal set

K13 is set

{K13} is non empty trivial finite 1 -element set

F \/ A is set

(F \/ A) \/ s is set

{D,K13} is non empty finite set

{D,K13} \/ s is non empty set

{D,K13,K11} is non empty finite set

card {D,K13,K11} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega

card S is epsilon-transitive epsilon-connected ordinal cardinal set

K12 is Element of bool X

card K12 is epsilon-transitive epsilon-connected ordinal cardinal set

card (b1 \/ B1) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

K11 is Element of bool X

card K11 is epsilon-transitive epsilon-connected ordinal cardinal set

card (b1 /\ B1) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

K11 is Element of bool X

card K11 is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

card ((A /\ s) \/ (X2 /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

(k - 2) + (2 * 1) is V27() V28() ext-real Element of REAL

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

(A /\ s) /\ (X2 /\ L) is set

card ((A /\ s) /\ (X2 /\ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

card ((X2 /\ L) \/ (b1 /\ B1)) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

(X2 /\ L) /\ (b1 /\ B1) is set

card ((X2 /\ L) /\ (b1 /\ B1)) is epsilon-transitive epsilon-connected ordinal cardinal set

card ((A /\ s) \/ (b1 /\ B1)) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

(A /\ s) /\ (b1 /\ B1) is set

card ((A /\ s) /\ (b1 /\ B1)) is epsilon-transitive epsilon-connected ordinal cardinal set

card ((C1 \/ b2) \/ a1) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of the Lines of (k,X)

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

card ((C1 \/ b2) \/ a1) is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of the Lines of (k,X)

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of bool X

card D is epsilon-transitive epsilon-connected ordinal cardinal set

K11 is Element of bool X

card K11 is epsilon-transitive epsilon-connected ordinal cardinal set

D is Element of the Lines of (k,X)

K11 is Element of the Lines of (k,X)

2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

D is Element of the Lines of (k,X)

K11 is Element of the Lines of (k,X)

k is IncProjStr

the Points of k is non empty set

bool the Points of k is non empty set

k is IncProjStr

the Points of k is non empty set

bool the Points of k is non empty set

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

X is non empty set

(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of (k,X) is non empty set

bool the Points of (k,X) is non empty set

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is non empty set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of (k,X) is non empty set

bool the Points of (k,X) is non empty set

k - 2 is V27() V28() ext-real Element of REAL

F is Element of bool the Points of (k,X)

succ k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

succ (k + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

(k + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

bool X is non empty set

{ b

the Lines of (k,X) is non empty set

{ b

k - 1 is V27() V28() ext-real Element of REAL

succ (k - 1) is non empty set

(k - 1) + 1 is V27() V28() ext-real Element of REAL

s is Element of bool X

card s is epsilon-transitive epsilon-connected ordinal cardinal set

{ b

succ (k - 2) is non empty set

(k - 2) + 1 is V27() V28() ext-real Element of REAL

A is Element of bool the Points of (k,X)

L is set

X2 is Element of the Points of (k,X)

s /\ L is Element of bool X

card (s /\ L) is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

L \/ s is set

X \ (L \/ s) is Element of bool X

B1 is set

{B1} is non empty trivial finite 1 -element set

s \/ {B1} is non empty set

card (s \/ {B1}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

b1 is Element of the Points of (k,X)

L /\ b1 is set

L /\ s is Element of bool X

C1 is set

card (L /\ b1) is epsilon-transitive epsilon-connected ordinal cardinal set

card (L /\ s) is epsilon-transitive epsilon-connected ordinal cardinal set

{X2,b1} is non empty finite Element of bool the Points of (k,X)

L \/ b1 is set

card (L \/ b1) is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of the Lines of (k,X)

C1 is Element of the Lines of (k,X)

b2 is Element of bool X

card b2 is epsilon-transitive epsilon-connected ordinal cardinal set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

(k - 1) + (2 * 1) is V27() V28() ext-real Element of REAL

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

b2 is Element of bool X

card b2 is epsilon-transitive epsilon-connected ordinal cardinal set

card L is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

L \ s is Element of bool L

bool L is non empty set

B1 is set

{B1} is non empty trivial finite 1 -element set

s \/ {B1} is non empty set

card (s \/ {B1}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

b1 is Element of bool X

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

b1 is Element of the Points of (k,X)

L \/ b1 is set

(L \/ s) \/ {B1} is non empty set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

{X2,b1} is non empty finite Element of bool the Points of (k,X)

C1 is Element of the Lines of (k,X)

C1 is Element of the Lines of (k,X)

card (L \/ b1) is epsilon-transitive epsilon-connected ordinal cardinal set

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

b2 is Element of bool X

card b2 is epsilon-transitive epsilon-connected ordinal cardinal set

A is Element of the Points of (k,X)

L is Element of the Points of (k,X)

{A,L} is non empty finite Element of bool the Points of (k,X)

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

A /\ L is set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

card (A /\ L) is epsilon-transitive epsilon-connected ordinal cardinal set

succ (card (A /\ L)) is non empty epsilon-transitive epsilon-connected ordinal set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

X \ A is Element of bool X

X2 is set

{X2} is non empty trivial finite 1 -element set

A \/ {X2} is non empty set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

card (A \/ {X2}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of the Lines of (k,X)

b1 is Element of bool X

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

A \/ L is set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

card (A \/ L) is epsilon-transitive epsilon-connected ordinal cardinal set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

(k - 1) + (2 * 1) is V27() V28() ext-real Element of REAL

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of the Lines of (k,X)

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of the Lines of (k,X)

B1 is Element of the Lines of (k,X)

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

s is Element of bool X

card s is epsilon-transitive epsilon-connected ordinal cardinal set

{ b

(k - 2) + 1 is V27() V28() ext-real Element of REAL

A is Element of bool the Points of (k,X)

L is set

X2 is Element of the Points of (k,X)

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

card L is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is set

b1 is Element of bool X

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

s \ L is Element of bool X

card (s \ L) is epsilon-transitive epsilon-connected ordinal cardinal set

s \ (s \ L) is Element of bool X

card (s \ (s \ L)) is epsilon-transitive epsilon-connected ordinal cardinal set

(k + 1) - 1 is V27() V28() ext-real Element of REAL

s /\ L is Element of bool X

b1 is Element of bool X

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

b1 is set

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

s \ b1 is Element of bool X

card (s \ b1) is epsilon-transitive epsilon-connected ordinal cardinal set

(k + 1) - 2 is V27() V28() ext-real Element of REAL

C1 is set

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

b1 \/ C1 is set

card (b1 \/ C1) is epsilon-transitive epsilon-connected ordinal cardinal set

2 + (k - 2) is V27() V28() ext-real Element of REAL

b2 is Element of the Points of (k,X)

b1 /\ L is set

L /\ b2 is set

L \/ b2 is set

card (L \/ b2) is epsilon-transitive epsilon-connected ordinal cardinal set

{B1} is non empty trivial finite 1 -element set

{B1} \/ b1 is non empty set

({B1} \/ b1) /\ (L /\ b2) is set

a1 is set

(L /\ b2) \/ {B1} is non empty set

((L /\ b2) \/ {B1}) \/ b1 is non empty set

(L /\ b2) \/ ({B1} \/ b1) is non empty set

card ((L /\ b2) \/ ({B1} \/ b1)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

a1 is Element of bool X

card a1 is epsilon-transitive epsilon-connected ordinal cardinal set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

(k - 1) + (2 * 1) is V27() V28() ext-real Element of REAL

2 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V27() V28() ext-real non positive non negative finite V57() cardinal {} -element Element of NAT

k + (2 * 0) is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

a1 is Element of bool X

card a1 is epsilon-transitive epsilon-connected ordinal cardinal set

card (L /\ b2) is epsilon-transitive epsilon-connected ordinal cardinal set

card ({B1} \/ b1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

(k - 1) + 3 is V27() V28() ext-real Element of REAL

k + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

{X2,b2} is non empty finite Element of bool the Points of (k,X)

a1 is Element of the Lines of (k,X)

a1 is Element of the Lines of (k,X)

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

S is Element of bool X

card S is epsilon-transitive epsilon-connected ordinal cardinal set

A is Element of the Points of (k,X)

L is Element of the Points of (k,X)

{A,L} is non empty finite Element of bool the Points of (k,X)

X2 is Element of the Lines of (k,X)

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT

k + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

X is non empty set

card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set

(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr

the Points of (k,X) is non empty set

bool the Points of (k,X) is non empty set

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

bool X is non empty set

{ b

succ (k + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

(k + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

F is Element of bool the Points of (k,X)

succ k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

card F is epsilon-transitive epsilon-connected ordinal cardinal set

succ (card F) is non empty epsilon-transitive epsilon-connected ordinal set

the Lines of (k,X) is non empty set

{ b

s is set

card s is epsilon-transitive epsilon-connected ordinal cardinal set

A is Element of the Points of (k,X)

card A is epsilon-transitive epsilon-connected ordinal cardinal set

X \ A is Element of bool X

L is set

{L} is non empty trivial finite 1 -element set

A \/ {L} is non empty set

card (A \/ {L}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of the Lines of (k,X)

{A} is non empty trivial finite 1 -element Element of bool the Points of (k,X)

B1 is Element of bool the Points of (k,X)

b1 is Element of the Points of (k,X)

C1 is Element of the Points of (k,X)

{b1,C1} is non empty finite Element of bool the Points of (k,X)

k - 1 is V27() V28() ext-real Element of REAL

s is set

{s} is non empty trivial finite 1 -element set

A is Element of the Points of (k,X)

L is Element of bool X

card L is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

L is Element of bool X

card L is epsilon-transitive epsilon-connected ordinal cardinal set

L is Element of bool X

card L is epsilon-transitive epsilon-connected ordinal cardinal set

X \ A is Element of bool X

L is set

{L} is non empty trivial finite 1 -element set

A \/ {L} is non empty set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

card (A \/ {L}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of bool X

card X2 is epsilon-transitive epsilon-connected ordinal cardinal set

X2 is Element of the Lines of (k,X)

(k - 1) + 1 is V27() V28() ext-real Element of REAL

B1 is Element of bool X

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 is set

card B1 is epsilon-transitive epsilon-connected ordinal cardinal set

b1 is Element of bool X

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

B1 \/ {L} is non empty set

card (B1 \/ {L}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

b1 is Element of the Points of (k,X)

{A,b1} is non empty finite Element of bool the Points of (k,X)

C1 is Element of bool the Points of (k,X)

b2 is Element of the Points of (k,X)

a1 is Element of the Points of (k,X)

{b2,a1} is non empty finite Element of bool the Points of (k,X)

succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT

s is set

card s is epsilon-transitive epsilon-connected ordinal cardinal set

A is set

L is set

{A,L} is non empty finite set

X2 is Element of the Points of (k,X)

B1 is Element of the Points of (k,X)

{X2,B1} is non empty finite Element of bool the Points of (k,X)

b1 is Element of the Lines of (k,X)

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

X2 /\ B1 is set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

X2 \/ B1 is set

card (X2 \/ B1) is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

b2 is Element of bool X

card b2 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

card b1 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool X

card C1 is epsilon-transitive epsilon-connected ordinal cardinal set

C1 is Element of bool