:: 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₁ where b₁ is Element of bool X : card b₁ = k } is set
{ b₁ where b₁ is Element of bool X : card b₁ = 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
[: { b₁ where b₁ is Element of bool X : card b₁ = k } , { b₁ where b₁ is Element of bool X : card b₁ = k + 1 } :] is set
(RelIncl (bool X)) /\ [: { b₁ where b₁ is Element of bool X : card b₁ = k } , { b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : card b₁ = k } is set
F is Element of the Points of (k,X)
{ b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : card b₁ = 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)
{ b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : card b₁ = k } is set
{ b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : card b₁ = k } is set
the Lines of (k,X) is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & s c= b₁ ) } 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
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & b₁ 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
{ b₁ where b₁ is Element of bool X : card b₁ = 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
{ b₁ where b₁ is Element of bool X : card b₁ = 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 X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
X \ b1 is Element of bool X
C1 is set
{C1} is non empty trivial finite 1 -element set
X2 /\ {C1} is finite set
B1 /\ {C1} is finite set
b2 is set
card X2 is epsilon-transitive epsilon-connected ordinal cardinal set
(k - 1) + 1 is V27() V28() ext-real Element of REAL
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
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
card (X2 /\ 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
X2 \ (X2 /\ B1) is Element of bool X2
bool X2 is non empty set
card (X2 \ (X2 /\ B1)) is epsilon-transitive epsilon-connected ordinal cardinal set
k - (k - 1) is V27() V28() ext-real Element of REAL
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is set
{b2} is non empty trivial finite 1 -element set
B1 \ (X2 /\ B1) is Element of bool B1
bool B1 is non empty set
card (B1 \ (X2 /\ B1)) is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is set
{a1} is non empty trivial finite 1 -element set
(X2 /\ B1) \/ {a1} is non empty 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
(X2 /\ B1) \/ {C1} is non empty set
card ((X2 /\ B1) \/ {C1}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
S is Element of the Points of (k,X)
B1 \/ S is set
ha1 is Element of bool X
card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set
X2 \/ S is set
ha1 is Element of bool X
card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set
B1 /\ S is set
B1 /\ X2 is set
B1 /\ (B1 /\ X2) is set
(B1 /\ {C1}) \/ (B1 /\ (B1 /\ X2)) is set
B1 /\ B1 is set
(B1 /\ B1) /\ X2 is set
(B1 /\ {C1}) \/ ((B1 /\ B1) /\ X2) is set
card (B1 /\ 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
card (B1 \/ 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 the Lines of (k,X)
X2 /\ S is set
X2 /\ (X2 /\ B1) is set
(X2 /\ {C1}) \/ (X2 /\ (X2 /\ B1)) is set
X2 /\ X2 is set
(X2 /\ X2) /\ B1 is set
(X2 /\ {C1}) \/ ((X2 /\ X2) /\ B1) is set
card (X2 /\ 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
card (X2 \/ 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 the Lines of (k,X)
{X2,B1,S} is non empty finite Element of bool the Points of (k,X)
S is Element of the Points of (k,X)
A2 is Element of the Points of (k,X)
{S,A2} is non empty finite Element of bool the Points of (k,X)
card {X2,B1} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
F \ {X2,B1} is Element of bool the Points of (k,X)
S is set
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 2 is V27() V28() ext-real Element of REAL
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
card B1 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 Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
y2 is Element of the Points of (k,X)
(X2 /\ B1) \/ {b2} is non empty set
(k + 1) - 1 is V27() V28() ext-real Element of REAL
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & X2 /\ B1 c= b₁ ) } is set
A1 is set
{X2,y2} is non empty finite Element of bool the Points of (k,X)
B2 is Element of the Lines of (k,X)
{B1,y2} is non empty finite Element of bool the Points of (k,X)
a2 is Element of the Lines of (k,X)
B1 \/ y2 is set
card (B1 \/ y2) 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 Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
B1 /\ y2 is set
card (B1 /\ y2) is epsilon-transitive epsilon-connected ordinal cardinal set
(X2 \/ B1) \/ y2 is set
card ((X2 \/ B1) \/ y2) is epsilon-transitive epsilon-connected ordinal cardinal set
X2 \/ y2 is set
card (X2 \/ y2) 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 Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
X2 /\ y2 is set
card (X2 /\ y2) is epsilon-transitive epsilon-connected ordinal cardinal set
(X2 /\ B1) /\ y2 is set
card ((X2 /\ B1) /\ y2) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 3 is V27() V28() ext-real Element of REAL
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
y2 \ (X2 /\ B1) is Element of bool y2
bool y2 is non empty set
card (y2 \ (X2 /\ B1)) is epsilon-transitive epsilon-connected ordinal cardinal set
A2 is set
{A2} is non empty trivial finite 1 -element set
(X2 /\ B1) \/ {A2} is non empty set
L3a is set
L3b is Element of bool X
card L3b is epsilon-transitive epsilon-connected ordinal cardinal set
D is Element of the Points of (k,X)
{X2,D} is non empty finite Element of bool the Points of (k,X)
K11 is Element of the Lines of (k,X)
card D is epsilon-transitive epsilon-connected ordinal cardinal set
{y2,D} is non empty finite Element of bool the Points of (k,X)
K13 is Element of the Lines of (k,X)
{B1,D} is non empty finite Element of bool the Points of (k,X)
K12 is Element of the Lines of (k,X)
X2 \/ D is set
card (X2 \/ D) is epsilon-transitive epsilon-connected ordinal cardinal set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
X2 /\ D is set
card (X2 /\ D) is epsilon-transitive epsilon-connected ordinal cardinal set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
(X2 /\ B1) /\ D is set
r is set
card ((X2 /\ B1) /\ D) is epsilon-transitive epsilon-connected ordinal cardinal set
B1 \/ D is set
card (B1 \/ D) is epsilon-transitive epsilon-connected ordinal cardinal set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
B1 /\ D is set
card (B1 /\ D) is epsilon-transitive epsilon-connected ordinal cardinal set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
y2 \/ D is set
card (y2 \/ D) is epsilon-transitive epsilon-connected ordinal cardinal set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
y2 /\ D is set
card (y2 /\ D) is epsilon-transitive epsilon-connected ordinal cardinal set
((X2 /\ B1) \/ {b2}) /\ D is set
((X2 /\ B1) \/ {a1}) /\ D is set
((X2 /\ B1) \/ {A2}) /\ D is set
{b2} /\ D is finite set
((X2 /\ B1) /\ D) \/ ({b2} /\ D) is set
{a1} /\ D is finite set
((X2 /\ B1) /\ D) \/ ({a1} /\ D) is set
{A2} /\ D is finite set
((X2 /\ B1) /\ D) \/ ({A2} /\ D) is set
r is Element of bool X
card r is epsilon-transitive epsilon-connected ordinal cardinal set
{b2,a1} is non empty finite set
{b2,a1} \/ {A2} is non empty finite set
{b2,a1,A2} is non empty finite set
((X2 /\ B1) /\ D) \/ {b2,a1,A2} is non empty set
{b2,a1,A2} /\ ((X2 /\ B1) /\ D) is finite set
r is set
((X2 /\ B1) \/ {b2}) /\ D is set
{b2} /\ D is finite set
((X2 /\ B1) /\ D) \/ ({b2} /\ D) is set
((X2 /\ B1) /\ D) \/ {b2} is non empty set
r is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
card {b2,a1,A2} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
card (((X2 /\ B1) /\ D) \/ {b2,a1,A2}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
k - 2 is V27() V28() ext-real Element of REAL
(k - 2) + 3 is V27() V28() ext-real Element of REAL
L3a is set
L3b is Element of bool X
card L3b is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool the Points of (k,X)
k - 2 is V27() V28() ext-real Element of REAL
succ (k - 2) is non empty set
(k - 2) + 1 is V27() V28() ext-real Element of REAL
card B1 is epsilon-transitive epsilon-connected ordinal cardinal set
(k - 1) + 1 is V27() V28() ext-real Element of REAL
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
card X2 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 Points of (k,X)
C1 is Element of the Points of (k,X)
X2 \/ C1 is set
card (X2 \/ 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
B1 \/ C1 is set
card (B1 \/ 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
b2 is Element of bool X
card b2 is 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
B1 /\ C1 is set
card (B1 /\ C1) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 2 is V27() V28() ext-real Element of REAL
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
X2 /\ C1 is set
card (X2 /\ 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
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
(X2 \/ B1) \/ C1 is set
card ((X2 \/ B1) \/ C1) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 1 is V27() V28() ext-real Element of REAL
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & b₁ c= b1 ) } is set
b2 is set
card (X2 /\ B1) is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
(X2 /\ B1) /\ C1 is set
card ((X2 /\ B1) /\ C1) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 3 is V27() V28() ext-real Element of REAL
a1 is Element of bool X
card 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
a1 is set
S is Element of bool X
card S is epsilon-transitive epsilon-connected ordinal cardinal set
ha1 is Element of the Points of (k,X)
ha1 is set
{ha1} is non empty trivial finite 1 -element set
card {ha1} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set
ha1 \ {ha1} is Element of bool ha1
bool ha1 is non empty set
card (ha1 \ {ha1}) is epsilon-transitive epsilon-connected ordinal cardinal set
{C1,ha1} is non empty finite Element of bool the Points of (k,X)
S is Element of the Lines of (k,X)
C1 \/ ha1 is set
card (C1 \/ ha1) is epsilon-transitive epsilon-connected ordinal cardinal set
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
C1 /\ ha1 is set
A2 is set
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
card (C1 /\ ha1) is epsilon-transitive epsilon-connected ordinal cardinal set
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
{B1,ha1} is non empty finite Element of bool the Points of (k,X)
A2 is Element of the Lines of (k,X)
{X2,ha1} is non empty finite Element of bool the Points of (k,X)
y2 is Element of the Lines of (k,X)
X2 \/ ha1 is set
card (X2 \/ ha1) is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
X2 /\ ha1 is set
A1 is set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
card (X2 /\ ha1) is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
B1 \/ ha1 is set
card (B1 \/ ha1) is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
B1 /\ ha1 is set
A1 is set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
card (B1 /\ ha1) is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
(X2 /\ ha1) /\ (B1 /\ ha1) is set
ha1 /\ B1 is set
X2 /\ (ha1 /\ B1) is set
(X2 /\ (ha1 /\ B1)) /\ ha1 is set
(X2 /\ B1) /\ ha1 is set
((X2 /\ B1) /\ ha1) /\ ha1 is set
ha1 /\ ha1 is set
(X2 /\ B1) /\ (ha1 /\ ha1) is set
((X2 /\ B1) /\ ha1) /\ (C1 /\ ha1) is set
ha1 /\ C1 is set
(X2 /\ B1) /\ (ha1 /\ C1) is set
((X2 /\ B1) /\ (ha1 /\ C1)) /\ ha1 is set
((X2 /\ B1) /\ C1) /\ ha1 is set
(((X2 /\ B1) /\ C1) /\ ha1) /\ ha1 is set
((X2 /\ B1) /\ C1) /\ (ha1 /\ ha1) is set
card (((X2 /\ B1) /\ C1) /\ ha1) is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is set
S is Element of bool X
card S is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool the Points of (k,X)
S is Element of bool X
card S is epsilon-transitive epsilon-connected ordinal cardinal set
C1 is Element of the Points of (k,X)
k is IncProjStr
X is IncProjStr
the Points of k is non empty set
the Points of X is non empty set
F is (k,X)
the of F is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
[: the Points of k, the Points of X:] is non empty set
bool [: the Points of k, the Points of X:] is non empty set
s is Element of the Points of k
the of F . s is Element of the Points of X
k is IncProjStr
X is IncProjStr
the Lines of k is non empty set
the Lines of X is non empty set
F is (k,X)
the of F is non empty Relation-like the Lines of k -defined the Lines of X -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of X:]
[: the Lines of k, the Lines of X:] is non empty set
bool [: the Lines of k, the Lines of X:] is non empty set
s is Element of the Lines of k
the of F . s is Element of the Lines of X
k is IncProjStr
X is IncProjStr
the Points of k is non empty set
the Lines of k is non empty set
F is (k,X)
s is (k,X)
the of F is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
the Points of X is non empty set
[: the Points of k, the Points of X:] is non empty set
bool [: the Points of k, the Points of X:] is non empty set
the of F is non empty Relation-like the Lines of k -defined the Lines of X -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of X:]
the Lines of X is non empty set
[: the Lines of k, the Lines of X:] is non empty set
bool [: the Lines of k, the Lines of X:] is non empty set
(k,X, the of F, the of F) is (k,X) (k,X)
the of s is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
the of s is non empty Relation-like the Lines of k -defined the Lines of X -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of X:]
(k,X, the of s, the of s) is (k,X) (k,X)
A is set
the of F . A is set
the of s . A is set
L is Element of the Points of k
(k,X,F,L) is Element of the Points of X
the of F . L is Element of the Points of X
(k,X,s,L) is Element of the Points of X
the of s . L is Element of the Points of X
A is set
the of F . A is set
the of s . A is set
L is Element of the Lines of k
(k,X,F,L) is Element of the Lines of X
the of F . L is Element of the Lines of X
(k,X,s,L) is Element of the Lines of X
the of s . L is Element of the Lines of X
k is IncProjStr
X is IncProjStr
k is IncProjStr
X is IncProjStr
F is (k,X)
the of F is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
the Points of k is non empty set
the Points of X is non empty set
[: the Points of k, the Points of X:] is non empty set
bool [: the Points of k, the Points of X:] is non empty set
the of F is non empty Relation-like the Lines of k -defined the Lines of X -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of X:]
the Lines of k is non empty set
the Lines of X is non empty set
[: the Lines of k, the Lines of X:] is non empty set
bool [: the Lines of k, the Lines of X:] is non empty set
(k,X, the of F, the of F) is (k,X) (k,X)
s is (k,X)
the of s is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
the of s is non empty Relation-like the Lines of k -defined the Lines of X -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of X:]
(k,X, the of s, the of s) is (k,X) (k,X)
A is Element of the Points of k
(k,X,s,A) is Element of the Points of X
the of s . A is Element of the Points of X
L is Element of the Lines of k
(k,X,s,L) is Element of the Lines of X
the of s . L is Element of the Lines of X
(k,X,F,A) is Element of the Points of X
the of F . A is Element of the Points of X
(k,X,F,L) is Element of the Lines of X
the of F . L is Element of the Lines of X
k is IncProjStr
k is IncProjStr
X is IncProjStr
the Points of k is non empty set
bool the Points of k is non empty set
F is (k,X)
the of F is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
the Points of X is non empty set
[: the Points of k, the Points of X:] is non empty set
bool [: the Points of k, the Points of X:] is non empty set
s is Element of bool the Points of k
the of F .: s is set
bool the Points of X is non empty set
A is set
dom the of F is Element of bool the Points of k
L is set
the of F . L is set
k is IncProjStr
X is IncProjStr
the Points of X is non empty set
bool the Points of X is non empty set
F is (k,X)
the of F is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
the Points of k is non empty set
[: the Points of k, the Points of X:] is non empty set
bool [: the Points of k, the Points of X:] is non empty set
s is Element of bool the Points of X
the of F " s is set
bool the Points of k is non empty set
A is set
dom the of F is Element of bool the Points of k
k is set
bool k is non empty set
X is finite set
card X is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(card X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool k : ( card b₁ = (card X) + 1 & X c= b₁ ) } is set
bool k is non empty Element of bool (bool k)
bool (bool k) is non empty set
bool (bool k) is non empty set
s is set
A is Element of bool k
card A 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
F is finite set
card F is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
k - 1 is V27() V28() ext-real Element of REAL
(X,F) is Element of bool (bool X)
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
(card F) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : ( card b₁ = (card F) + 1 & F c= b₁ ) } is 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
{ b₁ where b₁ is Element of bool X : card b₁ = k } is set
s is set
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
k is IncProjStr
X is IncProjStr
the Points of k is non empty set
bool the Points of k is non empty set
the Points of X is non empty set
F is (k,X)
s is Element of bool the Points of k
(k,X,F,s) is Element of bool the Points of X
bool the Points of X is non empty set
the of F is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
[: the Points of k, the Points of X:] is non empty set
bool [: the Points of k, the Points of X:] is non empty set
the of F .: s is set
{ b₁ where b₁ is Element of the Points of X : ex b₂ being Element of the Points of k st
( b₂ in s & (k,X,F,b₂) = b₁ ) } is set
L is set
dom the of F is Element of bool the Points of k
X2 is set
the of F . X2 is set
B1 is Element of the Points of k
b1 is Element of the Points of X
(k,X,F,B1) is Element of the Points of X
the of F . B1 is Element of the Points of X
L is set
dom the of F is Element of bool the Points of k
X2 is Element of the Points of X
B1 is Element of the Points of k
(k,X,F,B1) is Element of the Points of X
the of F . B1 is Element of the Points of X
k is IncProjStr
X is IncProjStr
the Points of X is non empty set
bool the Points of X is non empty set
the Points of k is non empty set
F is (k,X)
s is Element of bool the Points of X
(k,X,F,s) is Element of bool the Points of k
bool the Points of k is non empty set
the of F is non empty Relation-like the Points of k -defined the Points of X -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of X:]
[: the Points of k, the Points of X:] is non empty set
bool [: the Points of k, the Points of X:] is non empty set
the of F " s is set
{ b₁ where b₁ is Element of the Points of k : ex b₂ being Element of the Points of X st
( b₂ in s & (k,X,F,b₁) = b₂ ) } is set
L is set
X2 is Element of the Points of k
the of F . L is set
B1 is Element of the Points of X
(k,X,F,X2) is Element of the Points of X
the of F . X2 is Element of the Points of X
L is set
dom the of F is Element of bool the Points of k
X2 is Element of the Points of k
B1 is Element of the Points of X
(k,X,F,X2) is Element of the Points of X
the of F . X2 is Element of the Points of X
k is IncProjStr
the Points of k is non empty set
bool the Points of k is non empty set
X is (k,k)
F is Element of bool the Points of k
(k,k,X,F) is Element of bool the Points of k
the of X is non empty Relation-like the Points of k -defined the Points of k -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of k:]
[: the Points of k, the Points of k:] is non empty set
bool [: the Points of k, the Points of k:] is non empty set
the of X .: F is set
s is Element of the Points of k
A is Element of the Points of k
the Lines of k is non empty set
{s,A} is non empty finite Element of bool the Points of k
{ b₁ where b₁ is Element of the Points of k : ex b₂ being Element of the Points of k st
( b₂ in F & (k,k,X,b₂) = b₁ ) } is set
L is Element of the Points of k
X2 is Element of the Points of k
B1 is Element of the Points of k
(k,k,X,B1) is Element of the Points of k
the of X . B1 is Element of the Points of k
B1 is Element of the Points of k
(k,k,X,B1) is Element of the Points of k
the of X . B1 is Element of the Points of k
b1 is Element of the Points of k
(k,k,X,b1) is Element of the Points of k
the of X . b1 is Element of the Points of k
b1 is Element of the Points of k
(k,k,X,b1) is Element of the Points of k
the of X . b1 is Element of the Points of k
{b1,B1} is non empty finite Element of bool the Points of k
C1 is Element of the Lines of k
(k,k,X,C1) is Element of the Lines of k
the of X is non empty Relation-like the Lines of k -defined the Lines of k -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of k:]
[: the Lines of k, the Lines of k:] is non empty set
bool [: the Lines of k, the Lines of k:] is non empty set
the of X . C1 is Element of the Lines of k
k is IncProjStr
the Points of k is non empty set
bool the Points of k is non empty set
the Lines of k is non empty set
X is (k,k)
the of X is non empty Relation-like the Lines of k -defined the Lines of k -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of k:]
[: the Lines of k, the Lines of k:] is non empty set
bool [: the Lines of k, the Lines of k:] is non empty set
F is Element of bool the Points of k
(k,k,X,F) is Element of bool the Points of k
the of X is non empty Relation-like the Points of k -defined the Points of k -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of k:]
[: the Points of k, the Points of k:] is non empty set
bool [: the Points of k, the Points of k:] is non empty set
the of X " F is set
s is Element of the Points of k
A is Element of the Points of k
{s,A} is non empty finite Element of bool the Points of k
(k,k,X,s) is Element of the Points of k
the of X . s is Element of the Points of k
(k,k,X,A) is Element of the Points of k
the of X . A is Element of the Points of k
{(k,k,X,s),(k,k,X,A)} is non empty finite Element of bool the Points of k
L is Element of the Lines of k
rng the of X is set
dom the of X is Element of bool the Lines of k
bool the Lines of k is non empty set
X2 is set
the of X . X2 is set
B1 is Element of the Lines of k
(k,k,X,B1) is Element of the Lines of k
the of X . B1 is Element of the Lines of k
k is IncProjStr
the Points of k is non empty set
bool the Points of k is non empty set
X is (k,k)
F is Element of bool the Points of k
(k,k,X,F) is Element of bool the Points of k
the of X is non empty Relation-like the Points of k -defined the Points of k -valued Function-like V32( the Points of k) quasi_total Element of bool [: the Points of k, the Points of k:]
[: the Points of k, the Points of k:] is non empty set
bool [: the Points of k, the Points of k:] is non empty set
the of X .: F is set
(k,k,X,F) is Element of bool the Points of k
the of X " F is set
rng the of X is set
dom the of X is Element of bool the Points of k
s is Element of bool the Points of k
(k,k,X,(k,k,X,F)) is Element of bool the Points of k
the of X .: (k,k,X,F) is set
(k,k,X,s) is Element of bool the Points of k
the of X .: s is set
(k,k,X,(k,k,X,s)) is Element of bool the Points of k
the of X " (k,k,X,s) is set
the Lines of k is non empty set
the of X is non empty Relation-like the Lines of k -defined the Lines of k -valued Function-like V32( the Lines of k) quasi_total Element of bool [: the Lines of k, the Lines of k:]
[: the Lines of k, the Lines of k:] is non empty set
bool [: the Lines of k, the Lines of k:] is non empty set
(k,k,X,(k,k,X,F)) is Element of bool the Points of k
the of X " (k,k,X,F) is set
s is Element of bool the Points of k
(k,k,X,s) is Element of bool the Points of k
the of X " s is set
(k,k,X,(k,k,X,s)) is Element of bool the Points of k
the of X .: (k,k,X,s) is 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
F is ((k,X),(k,X))
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
2 - 1 is V27() V28() ext-real Element of REAL
s is Element of bool the Points of (k,X)
((k,X),(k,X),F,s) is Element of bool the Points of (k,X)
the of F is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
the of F .: s is set
((k,X),(k,X),F,s) is Element of bool the Points of (k,X)
the of F " s is 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₁ where b₁ is Element of bool X : card b₁ = k } is set
the Lines of (k,X) is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = k + 1 } is set
k + 0 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & b₁ c= A ) } is set
L is set
card L is epsilon-transitive epsilon-connected ordinal cardinal set
A \ L is Element of bool X
card (A \ L) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 1 is V27() V28() ext-real Element of REAL
X2 is set
card X2 is epsilon-transitive epsilon-connected ordinal cardinal set
B1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal set
A \ X2 is Element of bool X
card (A \ X2) is epsilon-transitive epsilon-connected ordinal cardinal set
b1 is Element of the Points of (k,X)
(A \ L) \ X2 is Element of bool X
card ((A \ L) \ X2) is epsilon-transitive epsilon-connected ordinal cardinal set
C1 is set
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
X2 \/ L is set
A \ (X2 \/ L) is Element of bool X
A \ C1 is Element of bool X
card (A \ C1) is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is Element of the Points of (k,X)
a1 is Element of the Lines of (k,X)
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
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & ha1 c= b₁ ) } is set
((k,X),(k,X),F,S) is Element of the Points of (k,X)
the of F . S is Element of the Points of (k,X)
ha1 is Element of the Points of (k,X)
(A \ X2) \ L is Element of bool X
((k,X),(k,X),F,b2) is Element of the Points of (k,X)
the of F . b2 is Element of the Points of (k,X)
S is Element of the Points of (k,X)
card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
((k,X),(k,X),F,b1) is Element of the Points of (k,X)
the of F . b1 is Element of the Points of (k,X)
A2 is Element of the Points of (k,X)
{ha1,A2} is non empty finite Element of bool the Points of (k,X)
y2 is Element of the Lines of (k,X)
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
ha1 /\ A2 is set
(ha1 /\ A2) /\ S is set
card ((ha1 /\ A2) /\ S) is epsilon-transitive epsilon-connected ordinal cardinal set
card (ha1 /\ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
((k,X),(k,X),F,a1) is Element of the Lines of (k,X)
the of F is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
the of F . a1 is Element of the Lines of (k,X)
A1 is Element of the Lines of (k,X)
ha1 \/ S is set
card (ha1 \/ S) 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 A2 is epsilon-transitive epsilon-connected ordinal cardinal set
B2 is Element of bool X
card B2 is epsilon-transitive epsilon-connected ordinal cardinal set
ha1 \/ A2 is set
card (ha1 \/ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
B2 is Element of bool X
card B2 is epsilon-transitive epsilon-connected ordinal cardinal set
dom the of F is Element of bool the Points of (k,X)
B2 is Element of bool X
card B2 is epsilon-transitive epsilon-connected ordinal cardinal set
a2 is Element of bool X
card a2 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
(k + 1) - 2 is V27() V28() ext-real Element of REAL
B2 is Element of bool X
card B2 is epsilon-transitive epsilon-connected ordinal cardinal set
{A2,S} is non empty finite Element of bool the Points of (k,X)
B2 is Element of the Lines of (k,X)
a2 is Element of bool X
card a2 is epsilon-transitive epsilon-connected ordinal cardinal set
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
ha1 /\ S is set
card (ha1 /\ 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
a2 is Element of bool X
card a2 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 Element of bool X
card a2 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 Element of bool X
card a2 is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 3 is V27() V28() ext-real Element of REAL
A2 \/ S is set
card (A2 \/ 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
a2 is Element of bool X
card a2 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 /\ S is set
card (A2 /\ 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
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
(ha1 \/ A2) \/ S is set
card ((ha1 \/ A2) \/ S) is epsilon-transitive epsilon-connected ordinal 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
a2 is Element of bool X
card a2 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 Element of bool X
card a2 is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 3 is V27() V28() ext-real Element of REAL
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & b₁ c= A ) } is set
L is Element of the Lines of (k,X)
the of F is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
rng the of F is set
dom the of F is Element of bool the Lines of (k,X)
bool the Lines of (k,X) is non empty set
X2 is set
the of F . X2 is set
B1 is Element of the Lines of (k,X)
((k,X),(k,X),F,B1) is Element of the Lines of (k,X)
the of F . B1 is Element of the Lines of (k,X)
b1 is set
card b1 is epsilon-transitive epsilon-connected ordinal cardinal set
A \ b1 is Element of bool X
card (A \ b1) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 1 is V27() V28() ext-real Element of REAL
C1 is set
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal set
(A \ b1) \ C1 is Element of bool X
card ((A \ b1) \ C1) is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is set
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
C1 \/ b1 is set
A \ (C1 \/ b1) is Element of bool X
A \ a1 is Element of bool X
card (A \ a1) is epsilon-transitive epsilon-connected ordinal cardinal set
S is Element of the Points of (k,X)
ha1 is Element of the Points of (k,X)
ha1 is Element of bool X
card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & ha1 c= b₁ ) } is set
rng the of F is set
dom the of F is Element of bool the Points of (k,X)
S is set
the of F . S is set
A2 is Element of the Points of (k,X)
y2 is set
the of F . y2 is set
A1 is Element of the Points of (k,X)
B2 is set
the of F . B2 is set
B2 is set
the of F . B2 is set
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
((k,X),(k,X),F,A1) is Element of the Points of (k,X)
the of F . A1 is Element of the Points of (k,X)
((k,X),(k,X),F,A2) is Element of the Points of (k,X)
the of F . A2 is Element of the Points of (k,X)
A1 \/ A2 is set
card (A1 \/ A2) 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 \ C1 is Element of bool X
(A \ C1) \ b1 is Element of bool X
B2 is Element of bool X
card B2 is epsilon-transitive epsilon-connected ordinal cardinal set
a2 is Element of bool X
card a2 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
A1 /\ A2 is set
card (A1 /\ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 2 is V27() V28() ext-real Element of REAL
B2 is Element of bool X
card B2 is epsilon-transitive epsilon-connected ordinal cardinal set
card (A \ C1) is epsilon-transitive epsilon-connected ordinal cardinal set
B2 is Element of the Points of (k,X)
a2 is set
the of F . a2 is set
A2 is Element of the Points of (k,X)
L3a is set
the of F . L3a is set
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
((k,X),(k,X),F,A2) is Element of the Points of (k,X)
the of F . A2 is Element of the Points of (k,X)
A1 \/ A2 is set
card (A1 \/ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
L3b is Element of bool X
card L3b is epsilon-transitive epsilon-connected ordinal cardinal set
A1 /\ A2 is set
card (A1 /\ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
A2 \/ A2 is set
card (A2 \/ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
L3b is Element of bool X
card L3b is epsilon-transitive epsilon-connected ordinal cardinal set
A2 /\ A2 is set
card (A2 /\ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
L3a is Element of bool X
card L3a is epsilon-transitive epsilon-connected ordinal cardinal set
{A1,A2} is non empty finite Element of bool the Points of (k,X)
L3a is Element of the Lines of (k,X)
L3b is Element of bool X
card L3b is epsilon-transitive epsilon-connected ordinal cardinal set
D is Element of bool X
card D is epsilon-transitive epsilon-connected ordinal cardinal set
(A1 /\ A2) /\ A2 is set
card ((A1 /\ A2) /\ A2) is epsilon-transitive epsilon-connected ordinal cardinal set
L3b is Element of bool X
card L3b is epsilon-transitive epsilon-connected ordinal cardinal set
D is Element of bool X
card D is epsilon-transitive epsilon-connected ordinal cardinal set
L3b is Element of bool X
card L3b is epsilon-transitive epsilon-connected ordinal cardinal set
{A2,A2} is non empty finite Element of bool the Points of (k,X)
L3b 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
(A1 \/ A2) \/ A2 is set
card ((A1 \/ A2) \/ A2) is epsilon-transitive epsilon-connected ordinal 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
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
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
[:X,X:] is non empty set
bool [:X,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
F is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
the Lines of (k,X) is non empty set
s is Relation-like Function-like set
dom s is set
bool X is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = k } is set
rng s is set
A is set
L is set
s . L is set
X2 is Element of bool X
card X2 is epsilon-transitive epsilon-connected ordinal cardinal set
F .: X2 is set
B1 is set
dom F is Element of bool X
rng F is set
b1 is set
F . b1 is set
dom F is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = k + 1 } is set
L is Relation-like Function-like set
dom L is set
rng L is set
X2 is set
B1 is set
L . B1 is set
b1 is Element of bool X
card b1 is epsilon-transitive epsilon-connected ordinal cardinal set
F .: b1 is set
C1 is set
dom F is Element of bool X
rng F is set
b2 is set
F . b2 is set
dom F is Element of bool X
card X2 is epsilon-transitive epsilon-connected ordinal cardinal set
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
A is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
X2 is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
((k,X),(k,X),A,X2) is ((k,X),(k,X)) ((k,X),(k,X))
B1 is Element of the Points of (k,X)
((k,X),(k,X),((k,X),(k,X),A,X2),B1) is Element of the Points of (k,X)
the of ((k,X),(k,X),A,X2) is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the of ((k,X),(k,X),A,X2) . B1 is Element of the Points of (k,X)
F .: B1 is set
b1 is Element of the Lines of (k,X)
((k,X),(k,X),((k,X),(k,X),A,X2),b1) is Element of the Lines of (k,X)
the of ((k,X),(k,X),A,X2) is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the of ((k,X),(k,X),A,X2) . b1 is Element of the Lines of (k,X)
F .: b1 is set
s is ((k,X),(k,X)) ((k,X),(k,X))
A is ((k,X),(k,X)) ((k,X),(k,X))
L is Element of the Lines of (k,X)
((k,X),(k,X),s,L) is Element of the Lines of (k,X)
the of s is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
the of s . L is Element of the Lines of (k,X)
((k,X),(k,X),A,L) is Element of the Lines of (k,X)
the of A is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the of A . L is Element of the Lines of (k,X)
F .: L is set
L is Element of the Points of (k,X)
((k,X),(k,X),s,L) is Element of the Points of (k,X)
the of s is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
the of s . L is Element of the Points of (k,X)
((k,X),(k,X),A,L) is Element of the Points of (k,X)
the of A is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the of A . L is Element of the Points of (k,X)
F .: L 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
[:X,X:] is non empty set
bool [:X,X:] is non empty set
the Points of (k,X) is non empty set
bool X is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = 1 } is set
F is Relation-like Function-like set
dom F is set
rng F is set
s is set
A is set
F . A is set
{A} is non empty trivial finite 1 -element set
card {A} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
s is ((k,X),(k,X))
the of s is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
the of s is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the Lines of (k,X) is non empty set
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
((k,X),(k,X), the of s, the of s) is ((k,X),(k,X)) ((k,X),(k,X))
[:X, the Points of (k,X):] is non empty set
bool [:X, the Points of (k,X):] is non empty set
A is non empty Relation-like X -defined the Points of (k,X) -valued Function-like V32(X) quasi_total Element of bool [:X, the Points of (k,X):]
L is Relation-like Function-like set
dom L is set
rng L is set
X2 is set
B1 is set
L . B1 is set
b1 is Element of X
A . b1 is Element of the Points of (k,X)
((k,X),(k,X),s,(A . b1)) is Element of the Points of (k,X)
the of s . (A . b1) is Element of the Points of (k,X)
union ((k,X),(k,X),s,(A . b1)) is set
C1 is Element of the Points of (k,X)
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is set
{b2} is non empty trivial finite 1 -element set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
dom the of s is Element of bool the Points of (k,X)
bool the Points of (k,X) is non empty set
X2 is non empty Relation-like X -defined X -valued Function-like V32(X) quasi_total Element of bool [:X,X:]
B1 is set
dom X2 is set
b1 is set
X2 . B1 is set
X2 . b1 is set
dom X2 is Element of bool X
C1 is Element of X
A . C1 is Element of the Points of (k,X)
((k,X),(k,X),s,(A . C1)) is Element of the Points of (k,X)
the of s . (A . C1) is Element of the Points of (k,X)
a1 is Element of the Points of (k,X)
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
{C1} is non empty trivial finite 1 -element Element of bool X
b2 is Element of X
A . b2 is Element of the Points of (k,X)
{b2} is non empty trivial finite 1 -element Element of bool X
((k,X),(k,X),s,(A . b2)) is Element of the Points of (k,X)
the of s . (A . b2) is Element of the Points of (k,X)
ha1 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 set
{ha1} is non empty trivial finite 1 -element set
X2 . b2 is Element of X
union ((k,X),(k,X),s,(A . b2)) is set
X2 . C1 is Element of X
union ((k,X),(k,X),s,(A . C1)) is set
rng the of s is set
B1 is set
{B1} is non empty trivial finite 1 -element set
card {B1} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
b1 is set
the of s . b1 is set
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
C1 is set
{C1} is non empty trivial finite 1 -element set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is Element of X
A . b2 is Element of the Points of (k,X)
((k,X),(k,X),s,(A . b2)) is Element of the Points of (k,X)
the of s . (A . b2) is Element of the Points of (k,X)
union ((k,X),(k,X),s,(A . b2)) is set
X2 . b2 is Element of X
rng X2 is set
dom the of s is Element of bool the Lines of (k,X)
bool the Lines of (k,X) is non empty set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : card b₁ = 1 + 1 } is set
B1 is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,B1) is ((k,X),(k,X)) ((k,X),(k,X))
the of (k,X,B1) is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
b1 is set
the of s . b1 is set
the of (k,X,B1) . b1 is set
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
a1 is set
S is set
{a1,S} is non empty finite set
ha1 is Element of X
A . ha1 is Element of the Points of (k,X)
{ha1} is non empty trivial finite 1 -element Element of bool X
S is Element of the Points of (k,X)
ha1 is Element of X
A . ha1 is Element of the Points of (k,X)
{ha1} is non empty trivial finite 1 -element Element of bool X
A2 is Element of the Points of (k,X)
((k,X),(k,X),s,S) is Element of the Points of (k,X)
the of s . S is Element of the Points of (k,X)
((k,X),(k,X),s,A2) is Element of the Points of (k,X)
the of s . A2 is Element of the Points of (k,X)
y2 is Element of bool X
card y2 is epsilon-transitive epsilon-connected ordinal cardinal set
y2 is set
{y2} is non empty trivial finite 1 -element set
((k,X),(k,X),s,C1) is Element of the Lines of (k,X)
the of s . C1 is Element of the Lines of (k,X)
((k,X),(k,X),(k,X,B1),C1) is Element of the Lines of (k,X)
the of (k,X,B1) . C1 is Element of the Lines of (k,X)
B1 .: C1 is set
S \/ A2 is set
B1 .: (S \/ A2) is set
B1 .: S is set
B1 .: A2 is set
(B1 .: S) \/ (B1 .: A2) is set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
((k,X),(k,X),s,(A . ha1)) is Element of the Points of (k,X)
the of s . (A . ha1) is Element of the Points of (k,X)
B1 . ha1 is Element of X
union ((k,X),(k,X),s,A2) is set
Im (B1,ha1) is set
{ha1} is non empty trivial finite 1 -element set
B1 .: {ha1} is finite set
{(B1 . ha1)} is non empty trivial finite 1 -element Element of bool X
A1 is Element of bool X
card A1 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
((k,X),(k,X),s,S) \/ ((k,X),(k,X),s,A2) is set
card (((k,X),(k,X),s,S) \/ ((k,X),(k,X),s,A2)) 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 set
{B2} is non empty trivial finite 1 -element set
((k,X),(k,X),s,(A . ha1)) is Element of the Points of (k,X)
the of s . (A . ha1) is Element of the Points of (k,X)
B1 . ha1 is Element of X
union ((k,X),(k,X),s,S) is set
Im (B1,ha1) is set
{ha1} is non empty trivial finite 1 -element set
B1 .: {ha1} is finite set
{(B1 . ha1)} is non empty trivial finite 1 -element Element of bool X
A1 is set
{A1} is non empty trivial finite 1 -element set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
A1 is Element of bool X
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
the of (k,X,B1) is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
b1 is set
the of s . b1 is set
the of (k,X,B1) . b1 is set
C1 is Element of the Points of (k,X)
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is set
{b2} is non empty trivial finite 1 -element set
S is Element of bool X
card S is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of X
A . a1 is Element of the Points of (k,X)
((k,X),(k,X),s,(A . a1)) is Element of the Points of (k,X)
the of s . (A . a1) is Element of the Points of (k,X)
((k,X),(k,X),s,C1) is Element of the Points of (k,X)
the of s . C1 is Element of the Points of (k,X)
B1 . a1 is Element of X
union ((k,X),(k,X),s,C1) is set
S is Element of bool X
card S is epsilon-transitive epsilon-connected ordinal cardinal set
((k,X),(k,X),(k,X,B1),C1) is Element of the Points of (k,X)
the of (k,X,B1) . C1 is Element of the Points of (k,X)
B1 .: C1 is set
Im (B1,a1) is set
{a1} is non empty trivial finite 1 -element set
B1 .: {a1} is finite set
{(B1 . a1)} is non empty trivial finite 1 -element Element of bool X
ha1 is set
{ha1} is non empty trivial finite 1 -element set
dom the of (k,X,B1) is Element of bool the Points of (k,X)
dom the of (k,X,B1) is Element of bool the Lines 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
[:X,X:] is non empty set
bool [:X,X:] is non empty set
bool X is non empty set
F is Relation-like Function-like set
dom F is set
the Points of (k,X) is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = k } is set
rng F is set
s is set
A is set
F . A is set
{A} is non empty trivial finite 1 -element set
card {A} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
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
s is ((k,X),(k,X))
the of s is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
the of s is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the Lines of (k,X) is non empty set
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
((k,X),(k,X), the of s, the of s) is ((k,X),(k,X)) ((k,X),(k,X))
[:X, the Points of (k,X):] is non empty set
bool [:X, the Points of (k,X):] is non empty set
A is non empty Relation-like X -defined the Points of (k,X) -valued Function-like V32(X) quasi_total Element of bool [:X, the Points of (k,X):]
L is Relation-like Function-like set
dom L is set
rng L is set
X2 is set
B1 is set
L . B1 is set
b1 is Element of X
A . b1 is Element of the Points of (k,X)
((k,X),(k,X),s,(A . b1)) is Element of the Points of (k,X)
the of s . (A . b1) is Element of the Points of (k,X)
X \ ((k,X),(k,X),s,(A . b1)) is Element of bool X
union (X \ ((k,X),(k,X),s,(A . b1))) is set
C1 is Element of the Points of (k,X)
X \ C1 is Element of bool X
card (X \ C1) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - k is V27() V28() ext-real Element of REAL
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is set
{b2} is non empty trivial finite 1 -element set
dom the of s is Element of bool the Points of (k,X)
bool the Points of (k,X) is non empty set
X2 is non empty Relation-like X -defined X -valued Function-like V32(X) quasi_total Element of bool [:X,X:]
B1 is set
dom X2 is set
b1 is set
X2 . B1 is set
X2 . b1 is set
dom X2 is Element of bool X
C1 is Element of X
A . C1 is Element of the Points of (k,X)
((k,X),(k,X),s,(A . C1)) is Element of the Points of (k,X)
the of s . (A . C1) is Element of the Points of (k,X)
a1 is Element of the Points of (k,X)
b2 is Element of X
A . b2 is Element of the Points of (k,X)
((k,X),(k,X),s,(A . b2)) is Element of the Points of (k,X)
the of s . (A . b2) is Element of the Points of (k,X)
S is Element of the Points of (k,X)
X \ S is Element of bool X
card (X \ S) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - k 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
X \ a1 is Element of bool X
card (X \ a1) 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
X2 . b2 is Element of X
X \ ((k,X),(k,X),s,(A . b2)) is Element of bool X
union (X \ ((k,X),(k,X),s,(A . b2))) is set
X2 . C1 is Element of X
X \ ((k,X),(k,X),s,(A . C1)) is Element of bool X
union (X \ ((k,X),(k,X),s,(A . C1))) is 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
{C1} is non empty trivial finite 1 -element Element of bool X
X \ {C1} is Element of bool X
{b2} is non empty trivial finite 1 -element Element of bool X
X \ {b2} is Element of bool X
rng the of s is set
B1 is set
{B1} is non empty trivial finite 1 -element set
card {B1} is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
X \ {B1} is Element of bool X
card (X \ {B1}) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - 1 is V27() V28() ext-real Element of REAL
b1 is set
the of s . b1 is set
X \ b1 is Element of bool X
card (X \ b1) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - k is V27() V28() ext-real Element of REAL
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
C1 is set
{C1} is non empty trivial finite 1 -element set
b1 /\ X is set
b2 is Element of X
{b2} is non empty trivial finite 1 -element Element of bool X
X \ {b2} is Element of bool X
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
A . b2 is Element of the Points of (k,X)
X /\ {B1} is finite set
((k,X),(k,X),s,(A . b2)) is Element of the Points of (k,X)
the of s . (A . b2) is Element of the Points of (k,X)
X \ ((k,X),(k,X),s,(A . b2)) is Element of bool X
union (X \ ((k,X),(k,X),s,(A . b2))) is set
X2 . b2 is Element of X
rng X2 is set
dom the of s is Element of bool the Lines of (k,X)
bool the Lines of (k,X) is non empty set
B1 is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,B1) is ((k,X),(k,X)) ((k,X),(k,X))
the of (k,X,B1) is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
b1 is set
the of s . b1 is set
the of (k,X,B1) . b1 is set
C1 is Element of the Points of (k,X)
((k,X),(k,X),s,C1) is Element of the Points of (k,X)
the of s . C1 is Element of the Points of (k,X)
X \ ((k,X),(k,X),s,C1) is Element of bool X
card (X \ ((k,X),(k,X),s,C1)) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 1) - k is V27() V28() ext-real Element of REAL
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
X \ (X \ ((k,X),(k,X),s,C1)) is Element of bool X
((k,X),(k,X),s,C1) /\ X is set
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
union (X \ ((k,X),(k,X),s,C1)) is set
{(union (X \ ((k,X),(k,X),s,C1)))} is non empty trivial finite 1 -element set
X \ {(union (X \ ((k,X),(k,X),s,C1)))} is Element of bool X
b2 is set
{b2} is non empty trivial finite 1 -element set
B1 .: X is set
X \ C1 is Element of bool X
X \ (X \ C1) is Element of bool X
C1 /\ X is set
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
card (X \ 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
b2 is set
{b2} is non empty trivial finite 1 -element set
a1 is Element of X
A . a1 is Element of the Points of (k,X)
{a1} is non empty trivial finite 1 -element Element of bool X
X \ {a1} is Element of bool X
Im (B1,a1) is set
{a1} is non empty trivial finite 1 -element set
B1 .: {a1} is finite set
B1 . a1 is Element of X
{(B1 . a1)} is non empty trivial finite 1 -element Element of bool X
((k,X),(k,X),(k,X,B1),C1) is Element of the Points of (k,X)
the of (k,X,B1) . C1 is Element of the Points of (k,X)
B1 .: C1 is set
B1 .: {a1} is finite set
(B1 .: X) \ (B1 .: {a1}) is Element of bool (B1 .: X)
bool (B1 .: X) is non empty set
dom the of (k,X,B1) is Element of bool the Points of (k,X)
{ b₁ where b₁ is Element of bool X : card b₁ = k + 1 } is set
the of (k,X,B1) is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
b1 is set
the of s . b1 is set
the of (k,X,B1) . b1 is set
C1 is Element of the Lines of (k,X)
((k,X),(k,X),s,C1) is Element of the Lines of (k,X)
the of s . 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
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
((k,X),(k,X),(k,X,B1),C1) is Element of the Lines of (k,X)
the of (k,X,B1) . C1 is Element of the Lines of (k,X)
B1 .: b1 is set
dom the of (k,X,B1) is Element of bool the Lines 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
k - 1 is V27() V28() ext-real Element of REAL
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
bool X is non empty set
F is Element of bool the Points of (k,X)
meet F is set
s is Element of bool X
card s is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & s c= b₁ ) } is set
X \ s is Element of bool X
1 + k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
- 1 is V27() V28() ext-real non positive Element of REAL
(- 1) + k is V27() V28() ext-real Element of REAL
A is set
{A} is non empty trivial finite 1 -element set
s \/ {A} is non empty set
card (s \/ {A}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
(k - 1) + 1 is V27() V28() ext-real Element of REAL
A is set
L is set
X2 is Element of bool X
card X2 is epsilon-transitive epsilon-connected ordinal cardinal set
X \ L is Element of bool X
X2 is Element of bool X
card X2 is epsilon-transitive epsilon-connected ordinal cardinal set
1 + k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
0 + k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT
X2 is set
{A} is non empty trivial finite 1 -element set
s /\ {A} is finite Element of bool X
B1 is set
L \ {A} is Element of bool L
bool L is non empty set
B1 is Element of bool X
card B1 is epsilon-transitive epsilon-connected ordinal cardinal set
{X2} is non empty trivial finite 1 -element set
(L \ {A}) \/ {X2} 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 (L \ {A}) 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 Element of bool X
card B1 is epsilon-transitive epsilon-connected ordinal cardinal set
card ((L \ {A}) \/ {X2}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
(k - 1) + 1 is V27() V28() ext-real Element of REAL
A is 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
k - 1 is V27() V28() ext-real Element of REAL
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
bool X is non empty set
F is Element of bool the Points of (k,X)
meet F is set
s is Element of bool X
card s is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & s c= b₁ ) } is set
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & A c= b₁ ) } 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
bool the Points of (k,X) is non empty set
F is Element of bool the Points of (k,X)
s is Element of bool the Points of (k,X)
meet F is set
meet s is set
bool X is non empty set
k - 1 is V27() V28() ext-real Element of REAL
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & A c= b₁ ) } is set
L is Element of bool X
card L is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k & L c= b₁ ) } 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
k - 1 is V27() V28() ext-real Element of REAL
X is non empty set
card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set
bool X is non empty set
F is finite Element of bool X
card F is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(k,X,F) is Element of bool the Points of (k,X)
(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
(X,F) is Element of bool (bool X)
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
bool (bool X) is non empty set
(card F) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : ( card b₁ = (card F) + 1 & F c= b₁ ) } 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
k - 1 is V27() V28() ext-real Element of REAL
X is non empty set
card X is non empty epsilon-transitive epsilon-connected ordinal cardinal set
bool X is non empty set
F is finite Element of bool X
card F is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(k,X,F) is Element of bool the Points of (k,X)
(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
meet (k,X,F) is set
(X,F) is Element of bool (bool X)
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
bool (bool X) is non empty set
(card F) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : ( card b₁ = (card F) + 1 & F c= b₁ ) } is set
k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT
k + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive 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 + 1),X) is strict with_non-trivial_lines up-2-rank IncProjStr
(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr
the Lines of (k,X) is non empty set
the Points of ((k + 1),X) is non empty set
the Points of (k,X) is non empty set
F is (((k + 1),X),((k + 1),X))
the of F is non empty Relation-like the Points of ((k + 1),X) -defined the Points of ((k + 1),X) -valued Function-like V32( the Points of ((k + 1),X)) quasi_total Element of bool [: the Points of ((k + 1),X), the Points of ((k + 1),X):]
[: the Points of ((k + 1),X), the Points of ((k + 1),X):] is non empty set
bool [: the Points of ((k + 1),X), the Points of ((k + 1),X):] is non empty set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
k + (1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
(k + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
(k + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
(k + 1) + 2 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₁ where b₁ is Element of bool X : card b₁ = k } is set
s is set
L is Element of bool X
card L is epsilon-transitive epsilon-connected ordinal cardinal set
A is finite Element of bool X
((k + 1),X,A) is Element of bool the Points of ((k + 1),X)
bool the Points of ((k + 1),X) is non empty set
(((k + 1),X),((k + 1),X),F,((k + 1),X,A)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,A) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,A)) is set
s is Relation-like Function-like set
dom s is set
{ b₁ where b₁ is Element of bool X : card b₁ = k + 1 } is set
k + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
rng s is set
L is set
X2 is set
s . X2 is set
B1 is finite set
((k + 1),X,B1) is Element of bool the Points of ((k + 1),X)
bool the Points of ((k + 1),X) is non empty set
(((k + 1),X),((k + 1),X),F,((k + 1),X,B1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,B1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,B1)) is set
card B1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(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 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
{ b₁ where b₁ is Element of bool X : ( card b₁ = k + 1 & b1 c= b₁ ) } is set
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
L is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
X2 is set
dom L is set
B1 is set
L . X2 is set
L . B1 is set
dom L is Element of bool the Points of (k,X)
bool the Points of (k,X) is non empty set
b1 is finite set
((k + 1),X,b1) is Element of bool the Points of ((k + 1),X)
bool the Points of ((k + 1),X) is non empty set
(((k + 1),X),((k + 1),X),F,((k + 1),X,b1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,b1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,b1)) is set
card b1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(k + 1) - 1 is V27() V28() ext-real Element of REAL
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
meet ((k + 1),X,b1) is 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 finite set
((k + 1),X,C1) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,C1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,C1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,C1)) is set
card C1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
meet ((k + 1),X,C1) is set
b2 is Element of bool X
card b2 is epsilon-transitive epsilon-connected ordinal cardinal set
A is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
((k,X),(k,X),L,A) is ((k,X),(k,X)) ((k,X),(k,X))
X2 is ((k,X),(k,X)) ((k,X),(k,X))
the of X2 is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
dom the of F is Element of bool the Points of ((k + 1),X)
bool the Points of ((k + 1),X) is non empty set
B1 is Element of the Points of (k,X)
((k,X),(k,X),X2,B1) is Element of the Points of (k,X)
the of X2 is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the of X2 . B1 is Element of the Points of (k,X)
b1 is Element of the Lines of (k,X)
((k,X),(k,X),X2,b1) is Element of the Lines of (k,X)
the of X2 . b1 is Element of the Lines of (k,X)
L . B1 is Element of the Points of (k,X)
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
b2 is Element of the Points of ((k + 1),X)
a1 is finite Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(k + 1) - 1 is V27() V28() ext-real Element of REAL
((k + 1),X,a1) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,a1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,a1) is set
(((k + 1),X),((k + 1),X),F,(((k + 1),X),((k + 1),X),F,((k + 1),X,a1))) is Element of bool the Points of ((k + 1),X)
the of F " (((k + 1),X),((k + 1),X),F,((k + 1),X,a1)) is set
S is Element of bool X
card S is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k + 1 & S c= b₁ ) } is set
ha1 is Element of bool X
card ha1 is epsilon-transitive epsilon-connected ordinal cardinal set
ha1 is finite Element of bool X
((k + 1),X,ha1) is Element of bool the Points of ((k + 1),X)
(X,ha1) is Element of bool (bool X)
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
bool (bool X) is non empty set
card ha1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(card ha1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : ( card b₁ = (card ha1) + 1 & ha1 c= b₁ ) } is set
(((k + 1),X),((k + 1),X),F,b2) is Element of the Points of ((k + 1),X)
the of F . b2 is Element of the Points of ((k + 1),X)
A2 is Element of bool X
card A2 is epsilon-transitive epsilon-connected ordinal cardinal set
(((k + 1),X),((k + 1),X),F,((k + 1),X,ha1)) is Element of bool the Points of ((k + 1),X)
the of F " ((k + 1),X,ha1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,ha1)) is set
S is finite Element of bool X
((k + 1),X,S) is Element of bool the Points of ((k + 1),X)
(X,S) is Element of bool (bool X)
card S is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(card S) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : ( card b₁ = (card S) + 1 & S c= b₁ ) } is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,a1)) is set
meet ((k + 1),X,a1) is set
A2 is finite set
((k + 1),X,A2) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,A2)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,A2) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,A2)) is set
((k + 1),X,a1) is Element of bool the Points of ((k + 1),X)
(X,a1) is Element of bool (bool X)
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
bool (bool X) is non empty set
(card a1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : ( card b₁ = (card a1) + 1 & a1 c= b₁ ) } is set
S is Element of bool X
card S is epsilon-transitive epsilon-connected ordinal cardinal set
(((k + 1),X),((k + 1),X),F,b2) is Element of the Points of ((k + 1),X)
the of F . b2 is Element of the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,a1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,a1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,a1)) is set
S is finite set
((k + 1),X,S) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,S)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,S) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,S)) is set
rng the of F is set
B1 is set
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
b1 is finite Element of bool X
card b1 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(k + 1) - 1 is V27() V28() ext-real Element of REAL
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
((k + 1),X,b1) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,b1)) is Element of bool the Points of ((k + 1),X)
the of F " ((k + 1),X,b1) is set
C1 is Element of bool X
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of bool X : ( card b₁ = k + 1 & C1 c= b₁ ) } is set
b2 is finite Element of bool X
L . b2 is set
((k + 1),X,b2) is Element of bool the Points of ((k + 1),X)
(X,b2) is Element of bool (bool X)
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
bool (bool X) is non empty set
card b2 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
(card b2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
{ b₁ where b₁ is Element of bool X : ( card b₁ = (card b2) + 1 & b2 c= b₁ ) } is set
meet ((k + 1),X,b1) is set
a1 is finite set
((k + 1),X,a1) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,a1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,a1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,a1)) is set
rng L is set
B1 is Element of the Points of (k,X)
L . B1 is Element of the Points of (k,X)
b1 is finite set
((k + 1),X,b1) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,b1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,b1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,b1)) is set
C1 is finite set
((k + 1),X,C1) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,C1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,C1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,C1)) is set
b1 is finite set
B1 is Element of the Points of (k,X)
((k,X),(k,X),X2,B1) is Element of the Points of (k,X)
the of X2 is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the of X2 . B1 is Element of the Points of (k,X)
((k + 1),X,b1) is Element of bool the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,((k + 1),X,b1)) is Element of bool the Points of ((k + 1),X)
the of F .: ((k + 1),X,b1) is set
meet (((k + 1),X),((k + 1),X),F,((k + 1),X,b1)) is set
k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT
k + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive 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 + 1),X) is strict with_non-trivial_lines up-2-rank IncProjStr
(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr
the Lines of (k,X) is non empty set
the Points of ((k + 1),X) is non empty set
[:X,X:] is non empty set
bool [:X,X:] is non empty set
bool X is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = k + 1 } is set
k + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
(k + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
k + 0 is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT
F is (((k + 1),X),((k + 1),X))
the of F is non empty Relation-like the Points of ((k + 1),X) -defined the Points of ((k + 1),X) -valued Function-like V32( the Points of ((k + 1),X)) quasi_total Element of bool [: the Points of ((k + 1),X), the Points of ((k + 1),X):]
[: the Points of ((k + 1),X), the Points of ((k + 1),X):] is non empty set
bool [: the Points of ((k + 1),X), the Points of ((k + 1),X):] is non empty set
the of F is non empty Relation-like the Lines of ((k + 1),X) -defined the Lines of ((k + 1),X) -valued Function-like V32( the Lines of ((k + 1),X)) quasi_total Element of bool [: the Lines of ((k + 1),X), the Lines of ((k + 1),X):]
the Lines of ((k + 1),X) is non empty set
[: the Lines of ((k + 1),X), the Lines of ((k + 1),X):] is non empty set
bool [: the Lines of ((k + 1),X), the Lines of ((k + 1),X):] is non empty set
(((k + 1),X),((k + 1),X), the of F, the of F) is (((k + 1),X),((k + 1),X)) (((k + 1),X),((k + 1),X))
s is ((k,X),(k,X))
the of s is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
the of s is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the Points of (k,X) is non empty set
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
((k,X),(k,X), the of s, the of s) is ((k,X),(k,X)) ((k,X),(k,X))
dom the of F is Element of bool the Points of ((k + 1),X)
bool the Points of ((k + 1),X) is non empty set
A is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,A) is ((k,X),(k,X)) ((k,X),(k,X))
((k + 1),X,A) is (((k + 1),X),((k + 1),X)) (((k + 1),X),((k + 1),X))
the of ((k + 1),X,A) is non empty Relation-like the Points of ((k + 1),X) -defined the Points of ((k + 1),X) -valued Function-like V32( the Points of ((k + 1),X)) quasi_total Element of bool [: the Points of ((k + 1),X), the Points of ((k + 1),X):]
L is set
the of F . L is set
the of ((k + 1),X,A) . L is set
X2 is Element of the Points of ((k + 1),X)
B1 is Element of the Lines of (k,X)
((k,X),(k,X),(k,X,A),B1) is Element of the Lines of (k,X)
the of (k,X,A) is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the of (k,X,A) . B1 is Element of the Lines of (k,X)
A .: B1 is set
(((k + 1),X),((k + 1),X),F,X2) is Element of the Points of ((k + 1),X)
the of F . X2 is Element of the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),((k + 1),X,A),X2) is Element of the Points of ((k + 1),X)
the of ((k + 1),X,A) . X2 is Element of the Points of ((k + 1),X)
{ b₁ where b₁ is Element of bool X : card b₁ = (k + 1) + 1 } is set
dom the of F is Element of bool the Lines of ((k + 1),X)
bool the Lines of ((k + 1),X) is non empty set
the of ((k + 1),X,A) is non empty Relation-like the Lines of ((k + 1),X) -defined the Lines of ((k + 1),X) -valued Function-like V32( the Lines of ((k + 1),X)) quasi_total Element of bool [: the Lines of ((k + 1),X), the Lines of ((k + 1),X):]
L is set
the of F . L is set
the of ((k + 1),X,A) . L is set
X2 is Element of the Lines of ((k + 1),X)
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
L \ B1 is Element of bool L
bool L is non empty set
card (L \ B1) is epsilon-transitive epsilon-connected ordinal cardinal set
(k + 2) - (k + 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 Element of bool X
card b1 is epsilon-transitive epsilon-connected ordinal cardinal set
b1 is Element of the Points of ((k + 1),X)
C1 is set
card C1 is epsilon-transitive epsilon-connected ordinal cardinal set
C1 \/ (L \ B1) is set
card (C1 \/ (L \ 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
b2 is Element of the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,b2) is Element of the Points of ((k + 1),X)
the of F . b2 is Element of the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),F,X2) is Element of the Lines of ((k + 1),X)
the of F . X2 is Element of the Lines of ((k + 1),X)
B1 \/ (C1 \/ (L \ B1)) is set
b1 \/ b2 is set
card (b1 \/ b2) is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
(L \ B1) /\ B1 is Element of bool L
card ((L \ B1) /\ B1) is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
(((k + 1),X),((k + 1),X),F,b1) is Element of the Points of ((k + 1),X)
the of F . b1 is Element of the Points of ((k + 1),X)
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
(((k + 1),X),((k + 1),X),F,b1) \/ (((k + 1),X),((k + 1),X),F,b2) is set
card ((((k + 1),X),((k + 1),X),F,b1) \/ (((k + 1),X),((k + 1),X),F,b2)) is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool X
card 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
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
a1 is Element of bool X
card a1 is epsilon-transitive epsilon-connected ordinal cardinal set
(((k + 1),X),((k + 1),X),((k + 1),X,A),X2) is Element of the Lines of ((k + 1),X)
the of ((k + 1),X,A) . X2 is Element of the Lines of ((k + 1),X)
A .: L is set
A .: b1 is set
A .: b2 is set
(A .: b1) \/ (A .: b2) is set
A .: (b1 \/ b2) is set
(((k + 1),X),((k + 1),X),((k + 1),X,A),b2) is Element of the Points of ((k + 1),X)
the of ((k + 1),X,A) . b2 is Element of the Points of ((k + 1),X)
(((k + 1),X),((k + 1),X),((k + 1),X,A),b1) is Element of the Points of ((k + 1),X)
the of ((k + 1),X,A) . b1 is Element of the Points of ((k + 1),X)
dom the of ((k + 1),X,A) is Element of bool the Lines of ((k + 1),X)
dom the of ((k + 1),X,A) is Element of bool the Points of ((k + 1),X)
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
[:X,X:] is non empty set
bool [:X,X:] is non empty set
F is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of NAT
(F,X) is strict with_non-trivial_lines up-2-rank IncProjStr
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
((F + 1),X) is strict with_non-trivial_lines up-2-rank IncProjStr
s is (((F + 1),X),((F + 1),X))
the of s is non empty Relation-like the Points of ((F + 1),X) -defined the Points of ((F + 1),X) -valued Function-like V32( the Points of ((F + 1),X)) quasi_total Element of bool [: the Points of ((F + 1),X), the Points of ((F + 1),X):]
the Points of ((F + 1),X) is non empty set
[: the Points of ((F + 1),X), the Points of ((F + 1),X):] is non empty set
bool [: the Points of ((F + 1),X), the Points of ((F + 1),X):] is non empty set
the of s is non empty Relation-like the Lines of ((F + 1),X) -defined the Lines of ((F + 1),X) -valued Function-like V32( the Lines of ((F + 1),X)) quasi_total Element of bool [: the Lines of ((F + 1),X), the Lines of ((F + 1),X):]
the Lines of ((F + 1),X) is non empty set
[: the Lines of ((F + 1),X), the Lines of ((F + 1),X):] is non empty set
bool [: the Lines of ((F + 1),X), the Lines of ((F + 1),X):] is non empty set
(((F + 1),X),((F + 1),X), the of s, the of s) is (((F + 1),X),((F + 1),X)) (((F + 1),X),((F + 1),X))
(F + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
F + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
F + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
(F + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
the Lines of (F,X) is non empty set
the Points of (F,X) is non empty set
A is ((F,X),(F,X))
the of A is non empty Relation-like the Lines of (F,X) -defined the Lines of (F,X) -valued Function-like V32( the Lines of (F,X)) quasi_total Element of bool [: the Lines of (F,X), the Lines of (F,X):]
[: the Lines of (F,X), the Lines of (F,X):] is non empty set
bool [: the Lines of (F,X), the Lines of (F,X):] is non empty set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
the of A is non empty Relation-like the Points of (F,X) -defined the Points of (F,X) -valued Function-like V32( the Points of (F,X)) quasi_total Element of bool [: the Points of (F,X), the Points of (F,X):]
[: the Points of (F,X), the Points of (F,X):] is non empty set
bool [: the Points of (F,X), the Points of (F,X):] is non empty set
((F,X),(F,X), the of A, the of A) is ((F,X),(F,X)) ((F,X),(F,X))
L is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(F,X,L) is ((F,X),(F,X)) ((F,X),(F,X))
((F + 1),X,L) is (((F + 1),X),((F + 1),X)) (((F + 1),X),((F + 1),X))
A is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
((F + 1),X,A) is (((F + 1),X),((F + 1),X)) (((F + 1),X),((F + 1),X))
L is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
((F + 1),X,L) is (((F + 1),X),((F + 1),X)) (((F + 1),X),((F + 1),X))
s is (((F + 1),X),((F + 1),X))
the of s is non empty Relation-like the Points of ((F + 1),X) -defined the Points of ((F + 1),X) -valued Function-like V32( the Points of ((F + 1),X)) quasi_total Element of bool [: the Points of ((F + 1),X), the Points of ((F + 1),X):]
the Points of ((F + 1),X) is non empty set
[: the Points of ((F + 1),X), the Points of ((F + 1),X):] is non empty set
bool [: the Points of ((F + 1),X), the Points of ((F + 1),X):] is non empty set
the of s is non empty Relation-like the Lines of ((F + 1),X) -defined the Lines of ((F + 1),X) -valued Function-like V32( the Lines of ((F + 1),X)) quasi_total Element of bool [: the Lines of ((F + 1),X), the Lines of ((F + 1),X):]
the Lines of ((F + 1),X) is non empty set
[: the Lines of ((F + 1),X), the Lines of ((F + 1),X):] is non empty set
bool [: the Lines of ((F + 1),X), the Lines of ((F + 1),X):] is non empty set
(((F + 1),X),((F + 1),X), the of s, the of s) is (((F + 1),X),((F + 1),X)) (((F + 1),X),((F + 1),X))
(0,X) is strict with_non-trivial_lines up-2-rank IncProjStr
F is ((0,X),(0,X))
the of F is non empty Relation-like the Points of (0,X) -defined the Points of (0,X) -valued Function-like V32( the Points of (0,X)) quasi_total Element of bool [: the Points of (0,X), the Points of (0,X):]
the Points of (0,X) is non empty set
[: the Points of (0,X), the Points of (0,X):] is non empty set
bool [: the Points of (0,X), the Points of (0,X):] is non empty set
the of F is non empty Relation-like the Lines of (0,X) -defined the Lines of (0,X) -valued Function-like V32( the Lines of (0,X)) quasi_total Element of bool [: the Lines of (0,X), the Lines of (0,X):]
the Lines of (0,X) is non empty set
[: the Lines of (0,X), the Lines of (0,X):] is non empty set
bool [: the Lines of (0,X), the Lines of (0,X):] is non empty set
((0,X),(0,X), the of F, the of F) is ((0,X),(0,X)) ((0,X),(0,X))
F is ((k,X),(k,X))
the of F is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the Points of (k,X) is non empty set
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
the of F is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the Lines of (k,X) is non empty set
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
((k,X),(k,X), the of F, the of F) is ((k,X),(k,X)) ((k,X),(k,X))
F is ((k,X),(k,X))
the of F is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the Points of (k,X) is non empty set
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
the of F is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the Lines of (k,X) is non empty set
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
((k,X),(k,X), the of F, the of F) is ((k,X),(k,X)) ((k,X),(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
[:X,X:] is non empty set
bool [:X,X:] is non empty set
(k,X) is strict with_non-trivial_lines up-2-rank IncProjStr
F is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,F) is ((k,X),(k,X)) ((k,X),(k,X))
the Points of (k,X) is non empty set
bool X is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = k } is set
the of (k,X,F) is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
s is set
dom the of (k,X,F) is set
A is set
the of (k,X,F) . s is set
the of (k,X,F) . A is set
dom the of (k,X,F) is Element of bool the Points of (k,X)
bool the Points of (k,X) is non empty set
L is Element of the Points of (k,X)
X2 is Element of the Points of (k,X)
((k,X),(k,X),(k,X,F),X2) is Element of the Points of (k,X)
the of (k,X,F) . X2 is Element of the Points of (k,X)
F .: A is set
((k,X),(k,X),(k,X,F),L) is Element of the Points of (k,X)
the of (k,X,F) . L is Element of the Points of (k,X)
F .: s is 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
s is set
F " s is set
dom F is Element of bool X
rng F is set
F .: (F " s) is set
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
card (F " s) is epsilon-transitive epsilon-connected ordinal cardinal set
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
A is Element of the Points of (k,X)
((k,X),(k,X),(k,X,F),A) is Element of the Points of (k,X)
the of (k,X,F) . A is Element of the Points of (k,X)
rng the of (k,X,F) is set
the Lines of (k,X) is non empty set
{ b₁ where b₁ is Element of bool X : card b₁ = k + 1 } is set
the of (k,X,F) is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
s is set
F " s is set
dom F is Element of bool X
rng F is set
F .: (F " s) is set
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
card (F " s) is epsilon-transitive epsilon-connected ordinal cardinal set
A is Element of bool X
card A is epsilon-transitive epsilon-connected ordinal cardinal set
A is Element of the Lines of (k,X)
((k,X),(k,X),(k,X,F),A) is Element of the Lines of (k,X)
the of (k,X,F) . A is Element of the Lines of (k,X)
rng the of (k,X,F) is set
dom F is Element of bool X
s is Element of the Points of (k,X)
((k,X),(k,X),(k,X,F),s) is Element of the Points of (k,X)
the of (k,X,F) . s is Element of the Points of (k,X)
A is Element of the Lines of (k,X)
((k,X),(k,X),(k,X,F),A) is Element of the Lines of (k,X)
the of (k,X,F) . A is Element of the Lines of (k,X)
F .: s is set
F .: A is set
L is Element of bool X
card L is epsilon-transitive epsilon-connected ordinal cardinal set
s is set
dom the of (k,X,F) is set
A is set
the of (k,X,F) . s is set
the of (k,X,F) . A is set
dom the of (k,X,F) is Element of bool the Lines of (k,X)
bool the Lines of (k,X) is non empty set
L is Element of the Lines of (k,X)
X2 is Element of the Lines of (k,X)
((k,X),(k,X),(k,X,F),X2) is Element of the Lines of (k,X)
the of (k,X,F) . X2 is Element of the Lines of (k,X)
F .: A is set
((k,X),(k,X),(k,X,F),L) is Element of the Lines of (k,X)
the of (k,X,F) . L is Element of the Lines of (k,X)
F .: s is 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
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
[:X,X:] is non empty set
bool [:X,X:] is non empty set
F is ((k,X),(k,X))
the of F is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the Points of (k,X) is non empty set
[: the Points of (k,X), the Points of (k,X):] is non empty set
bool [: the Points of (k,X), the Points of (k,X):] is non empty set
the of F is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the Lines of (k,X) is non empty set
[: the Lines of (k,X), the Lines of (k,X):] is non empty set
bool [: the Lines of (k,X), the Lines of (k,X):] is non empty set
((k,X),(k,X), the of F, the of F) is ((k,X),(k,X)) ((k,X),(k,X))
card k is epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real non negative finite cardinal Element of omega
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
card (k + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
succ (card X) is non empty epsilon-transitive epsilon-connected ordinal set
card 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of omega
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
succ k is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal 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
k + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() V28() ext-real positive non negative finite cardinal Element of NAT
s is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,s) is ((k,X),(k,X)) ((k,X),(k,X))
s is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,s) is ((k,X),(k,X)) ((k,X),(k,X))
A is Element of the Points of (k,X)
((k,X),(k,X),F,A) is Element of the Points of (k,X)
the of F . A is Element of the Points of (k,X)
L is Element of the Lines of (k,X)
((k,X),(k,X),F,L) is Element of the Lines of (k,X)
the of F . L is Element of the Lines of (k,X)
((k,X),(k,X),(k,X,s),A) is Element of the Points of (k,X)
the of (k,X,s) is non empty Relation-like the Points of (k,X) -defined the Points of (k,X) -valued Function-like V32( the Points of (k,X)) quasi_total Element of bool [: the Points of (k,X), the Points of (k,X):]
the of (k,X,s) . A is Element of the Points of (k,X)
((k,X),(k,X),(k,X,s),L) is Element of the Lines of (k,X)
the of (k,X,s) is non empty Relation-like the Lines of (k,X) -defined the Lines of (k,X) -valued Function-like V32( the Lines of (k,X)) quasi_total Element of bool [: the Lines of (k,X), the Lines of (k,X):]
the of (k,X,s) . L is Element of the Lines of (k,X)
s is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,s) is ((k,X),(k,X)) ((k,X),(k,X))
A is non empty Relation-like X -defined X -valued Function-like one-to-one V32(X) quasi_total onto bijective Element of bool [:X,X:]
(k,X,A) is ((k,X),(k,X)) ((k,X),(k,X))