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
{ b1 where b1 is Element of bool X : card b1 = k } is set
{ b1 where b1 is Element of bool X : card b1 = k + 1 } is 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
[: { b1 where b1 is Element of bool X : card b1 = k } , { b1 where b1 is Element of bool X : card b1 = k + 1 } :] is set
(RelIncl (bool X)) /\ [: { b1 where b1 is Element of bool X : card b1 = k } , { b1 where b1 is Element of bool X : card b1 = k + 1 } :] is set
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
{ b1 where b1 is Element of bool X : card b1 = k } is set
F is Element of the Points of (k,X)
{ b1 where b1 is Element of bool X : card b1 = k + 1 } is set
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
{ b1 where b1 is Element of bool X : card b1 = k } is 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)
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)
{ b1 where b1 is Element of bool X : card b1 = k + 1 } is set
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
{ b1 where b1 is Element of bool X : card b1 = k } is set
{ b1 where b1 is Element of bool X : card b1 = k + 1 } is 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)
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
{ b1 where b1 is Element of bool X : card b1 = k + 1 } is set
{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
{ b1 where b1 is Element of bool X : card b1 = k } is set
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
{ b1 where b1 is Element of bool X : card b1 = k } is set
the Lines of (k,X) is non empty set
{ b1 where b1 is Element of bool X : card b1 = k + 1 } is set
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
{ b1 where b1 is Element of bool X : ( card b1 = k & s c= b1 ) } is set
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
{ b1 where b1 is Element of bool X : ( card b1 = k & b1 c= s ) } is 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)
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
{ b1 where b1 is Element of bool X : card b1 = k } is set
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
{ b1 where b1 is Element of bool X : card b1 = k + 1 } is set
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