:: PROJRED2 semantic presentation

K99() is set
bool K99() is set

the Lines of IPP is V4() set

the Lines of IPP is V4() set
the Points of IPP is V4() set
a is Element of the Lines of IPP
{ b1 where b1 is Element of the Points of IPP : b1 on a } is set
bool the Points of IPP is set
q is set
A is Element of the Points of IPP

the Points of IPP is V4() set
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
the Lines of IPP is V4() set
the Element of the Lines of IPP is Element of the Lines of IPP
b is Element of the Points of IPP
IncProj ( the Element of the Lines of IPP,b, the Element of the Lines of IPP) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]

the Lines of IPP is V4() set
a is Element of the Lines of IPP
b is Element of the Lines of IPP
q is Element of the Lines of IPP
the Points of IPP is V4() set
A is Element of the Points of IPP
B is Element of the Points of IPP

the Lines of IPP is V4() set
a is Element of the Lines of IPP
b is Element of the Lines of IPP
q is Element of the Lines of IPP
the Points of IPP is V4() set
A is Element of the Points of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Lines of IPP
A is Element of the Lines of IPP
IncProj (q,a,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
B is Element of the Lines of IPP
C is Element of the Points of IPP
(IncProj (q,a,A)) . C is set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Lines of IPP
(IPP,b) is Element of bool the Points of IPP
bool the Points of IPP is set
{ b1 where b1 is Element of the Points of IPP : b1 on b } is set
q is Element of the Lines of IPP
IncProj (b,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
dom (IncProj (b,a,q)) is Element of bool the Points of IPP
A is set
B is Element of the Points of IPP
A is set
B is Element of the Points of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Lines of IPP
q is Element of the Lines of IPP
IncProj (b,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
rng (IncProj (b,a,q)) is set
(IPP,q) is Element of bool the Points of IPP
bool the Points of IPP is set
{ b1 where b1 is Element of the Points of IPP : b1 on q } is set
A is set
B is Element of the Points of IPP
C is Element of the Points of IPP
C is Element of the Points of IPP
(IncProj (b,a,q)) . C is set
(IPP,b) is Element of bool the Points of IPP
{ b1 where b1 is Element of the Points of IPP : b1 on b } is set
dom (IncProj (b,a,q)) is Element of bool the Points of IPP
A is set
B is Element of the Points of IPP

the Lines of IPP is V4() set

the Lines of q is V4() set
the Points of q is V4() set
b is set
a is Element of the Lines of IPP
(IPP,a) is Element of bool the Points of IPP
the Points of IPP is V4() set
bool the Points of IPP is set
{ b1 where b1 is Element of the Points of IPP : b1 on a } is set
B is set
C is Element of the Points of q
A is Element of the Lines of q
(q,A) is Element of bool the Points of q
bool the Points of q is set
{ b1 where b1 is Element of the Points of q : b1 on A } is set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Lines of IPP
q is Element of the Lines of IPP
IncProj (b,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
B is set
dom (IncProj (b,a,q)) is Element of bool the Points of IPP
bool the Points of IPP is set
C is set
(IncProj (b,a,q)) . B is set
(IncProj (b,a,q)) . C is set
(IPP,b) is Element of bool the Points of IPP
{ b1 where b1 is Element of the Points of IPP : b1 on b } is set
O is Element of the Points of IPP
Q is Element of the Points of IPP
(IncProj (b,a,q)) . O is set
(IncProj (b,a,q)) . Q is set
c10 is Element of the Points of IPP
Q is Element of the Points of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Lines of IPP
q is Element of the Lines of IPP
IncProj (b,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
(IncProj (b,a,q)) " is Relation-like Function-like set
IncProj (q,a,b) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
rng (IncProj (b,a,q)) is set
(IPP,q) is Element of bool the Points of IPP
bool the Points of IPP is set
{ b1 where b1 is Element of the Points of IPP : b1 on q } is set
dom (IncProj (b,a,q)) is Element of bool the Points of IPP
(IPP,b) is Element of bool the Points of IPP
{ b1 where b1 is Element of the Points of IPP : b1 on b } is set
O is set
C is set
(IncProj (b,a,q)) . O is set
Q is Element of the Points of IPP
c10 is Element of the Points of IPP
(IncProj (q,a,b)) . C is set
Q is Element of the Lines of IPP
Q is Element of the Points of IPP
c10 is Element of the Points of IPP
Q is Element of the Lines of IPP
dom (IncProj (q,a,b)) is Element of bool the Points of IPP

the Points of IPP is V4() set
a is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like (IPP)

the Lines of IPP is V4() set
b is Element of the Points of IPP
q is Element of the Lines of IPP
A is Element of the Lines of IPP
IncProj (q,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (A,b,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Lines of IPP
IncProj (b,a,b) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
(IPP,b) is Element of bool the Points of IPP
bool the Points of IPP is set
{ b1 where b1 is Element of the Points of IPP : b1 on b } is set
id (IPP,b) is Relation-like (IPP,b) -defined (IPP,b) -valued Function-like one-to-one total Element of bool [:(IPP,b),(IPP,b):]
[:(IPP,b),(IPP,b):] is set
bool [:(IPP,b),(IPP,b):] is set
A is set
(IncProj (b,a,b)) . A is set
B is Element of the Points of IPP
dom (IncProj (b,a,b)) is Element of bool the Points of IPP

the Lines of IPP is V4() set
the Points of IPP is V4() set
a is Element of the Lines of IPP
(IPP,a) is Element of bool the Points of IPP
bool the Points of IPP is set
{ b1 where b1 is Element of the Points of IPP : b1 on a } is set
id (IPP,a) is Relation-like (IPP,a) -defined (IPP,a) -valued Function-like one-to-one total Element of bool [:(IPP,a),(IPP,a):]
[:(IPP,a),(IPP,a):] is set
bool [:(IPP,a),(IPP,a):] is set
b is Element of the Points of IPP
IncProj (a,b,a) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Lines of IPP
q is Element of the Lines of IPP
IncProj (b,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
A is Element of the Lines of IPP
IncProj (b,a,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (A,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (b,a,A)) * (IncProj (A,a,q)) is Relation-like Function-like set
dom (IncProj (b,a,q)) is Element of bool the Points of IPP
bool the Points of IPP is set
(IPP,b) is Element of bool the Points of IPP
{ b1 where b1 is Element of the Points of IPP : b1 on b } is set
dom (IncProj (b,a,A)) is Element of bool the Points of IPP
c10 is Element of the Points of IPP
(IncProj (b,a,q)) . c10 is set
((IncProj (b,a,A)) * (IncProj (A,a,q))) . c10 is set
Q is Element of the Lines of IPP
O1 is Element of the Points of IPP
(IncProj (b,a,A)) . c10 is set
o9 is Element of the Points of IPP
(IncProj (A,a,q)) . ((IncProj (b,a,A)) . c10) is set
c10 is set
((IncProj (b,a,A)) * (IncProj (A,a,q))) . c10 is set
(IncProj (b,a,q)) . c10 is set
Q is Element of the Points of IPP
dom ((IncProj (b,a,A)) * (IncProj (A,a,q))) is set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Lines of IPP
A is Element of the Lines of IPP
IncProj (q,a,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
B is Element of the Lines of IPP
IncProj (A,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,a,A)) * (IncProj (A,b,B)) is Relation-like Function-like set
C is Element of the Points of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
B is Element of the Points of IPP
C is Element of the Points of IPP
O is Element of the Points of IPP
Q is Element of the Lines of IPP
c10 is Element of the Lines of IPP
Q is Element of the Lines of IPP
IncProj (Q,a,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (Q,b,c10) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (Q,a,Q)) * (IncProj (Q,b,c10)) is Relation-like Function-like set
O1 is Element of the Lines of IPP
IncProj (Q,C,O1) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (O1,b,c10) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (Q,C,O1)) * (IncProj (O1,b,c10)) is Relation-like Function-like set
o9 is Element of the Lines of IPP
O2 is Element of the Lines of IPP
O3 is Element of the Lines of IPP
o99 is Element of the Lines of IPP
dom (IncProj (Q,a,Q)) is Element of bool the Points of IPP
bool the Points of IPP is set
(IPP,Q) is Element of bool the Points of IPP
{ b1 where b1 is Element of the Points of IPP : b1 on Q } is set
dom (IncProj (Q,C,O1)) is Element of bool the Points of IPP
dom ((IncProj (Q,C,O1)) * (IncProj (O1,b,c10))) is set
x99 is Element of the Points of IPP
((IncProj (Q,a,Q)) * (IncProj (Q,b,c10))) . x99 is set
((IncProj (Q,C,O1)) * (IncProj (O1,b,c10))) . x99 is set
O1 is Element of the Lines of IPP
O3 is Element of the Lines of IPP
O2 is Element of the Points of IPP
O4 is Element of the Points of IPP
{O,O2,q} is Element of bool the Points of IPP
{A,O4,q} is Element of bool the Points of IPP
{B,O,C} is Element of bool the Points of IPP
{O,A,b} is Element of bool the Points of IPP
{b,a,C} is Element of bool the Points of IPP
{x99,O2,C} is Element of bool the Points of IPP
{B,x99,q} is Element of bool the Points of IPP
{B,A,a} is Element of bool the Points of IPP
{x99,O4,a} is Element of bool the Points of IPP
{O2,O4,b} is Element of bool the Points of IPP
Q2 is Element of the Lines of IPP
y is Element of the Points of IPP
(IncProj (Q,b,c10)) . O4 is set
(IncProj (O1,b,c10)) . O2 is set
(IncProj (Q,a,Q)) . x99 is set
(IncProj (Q,C,O1)) . x99 is set
(IncProj (O1,b,c10)) . ((IncProj (Q,C,O1)) . x99) is set
(IncProj (Q,C,O1)) . B is set
(IncProj (O1,b,c10)) . O is set
(IncProj (Q,a,Q)) . B is set
(IncProj (Q,b,c10)) . A is set
x99 is set
((IncProj (Q,a,Q)) * (IncProj (Q,b,c10))) . x99 is set
((IncProj (Q,C,O1)) * (IncProj (O1,b,c10))) . x99 is set
O1 is Element of the Points of IPP
dom ((IncProj (Q,a,Q)) * (IncProj (Q,b,c10))) is set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
B is Element of the Points of IPP
{A,B} is Element of bool the Points of IPP
bool the Points of IPP is set
C is Element of the Points of IPP
O is Element of the Points of IPP
{B,C,O} is Element of bool the Points of IPP
{a,b,O} is Element of bool the Points of IPP
Q is Element of the Points of IPP
{A,O,Q} is Element of bool the Points of IPP
{a,B,Q} is Element of bool the Points of IPP
c10 is Element of the Points of IPP
{A,c10} is Element of bool the Points of IPP
{b,Q,c10} is Element of bool the Points of IPP
{B,c10,q} is Element of bool the Points of IPP
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
IncProj (Q,a,O1) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
o9 is Element of the Lines of IPP
IncProj (O1,b,o9) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (Q,a,O1)) * (IncProj (O1,b,o9)) is Relation-like Function-like set
O2 is Element of the Lines of IPP
IncProj (Q,q,O2) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (O2,b,o9) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (Q,q,O2)) * (IncProj (O2,b,o9)) is Relation-like Function-like set
O3 is Element of the Lines of IPP
o99 is Element of the Lines of IPP
oo9 is Element of the Lines of IPP
Q is Element of the Lines of IPP
(IPP,Q) is Element of bool the Points of IPP
{ b1 where b1 is Element of the Points of IPP : b1 on Q } is set
dom (IncProj (Q,a,O1)) is Element of bool the Points of IPP
dom (IncProj (Q,q,O2)) is Element of bool the Points of IPP
dom ((IncProj (Q,q,O2)) * (IncProj (O2,b,o9))) is set
{Q,b,c10} is Element of bool the Points of IPP
{Q,B,a} is Element of bool the Points of IPP
{B,q,c10} is Element of bool the Points of IPP
{b,q,a} is Element of bool the Points of IPP
O3 is Element of the Points of IPP
((IncProj (Q,a,O1)) * (IncProj (O1,b,o9))) . O3 is set
((IncProj (Q,q,O2)) * (IncProj (O2,b,o9))) . O3 is set
{A,B,O3} is Element of bool the Points of IPP
O2 is Element of the Lines of IPP
O4 is Element of the Points of IPP
{O3,a,O4} is Element of bool the Points of IPP
{Q,A,O4} is Element of bool the Points of IPP
Q2 is Element of the Lines of IPP
y is Element of the Points of IPP
{A,y,c10} is Element of bool the Points of IPP
{b,y,O4} is Element of bool the Points of IPP
{y,q,O3} is Element of bool the Points of IPP
R is Element of the Lines of IPP
(IncProj (Q,q,O2)) . O3 is set
x99 is Element of the Points of IPP
(IncProj (O2,b,o9)) . y is set
(IncProj (O1,b,o9)) . O4 is set
(IncProj (Q,a,O1)) . O3 is set
(IncProj (O2,b,o9)) . ((IncProj (Q,q,O2)) . O3) is set
O3 is set
((IncProj (Q,a,O1)) * (IncProj (O1,b,o9))) . O3 is set
((IncProj (Q,q,O2)) * (IncProj (O2,b,o9))) . O3 is set
O2 is Element of the Points of IPP
dom ((IncProj (Q,a,O1)) * (IncProj (O1,b,o9))) is set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
{q,A} is Element of bool the Points of IPP
bool the Points of IPP is set
B is Element of the Points of IPP
{q,B} is Element of bool the Points of IPP
{a,B,A} is Element of bool the Points of IPP
C is Element of the Points of IPP
{a,b,C} is Element of bool the Points of IPP
O is Element of the Points of IPP
{q,O} is Element of bool the Points of IPP
{C,A,O} is Element of bool the Points of IPP
{b,B,O} is Element of bool the Points of IPP
Q is Element of the Lines of IPP
c10 is Element of the Lines of IPP
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Lines of IPP
O2 is Element of the Lines of IPP
O3 is Element of the Lines of IPP
o99 is Element of the Lines of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
{q,A} is Element of bool the Points of IPP
bool the Points of IPP is set
B is Element of the Points of IPP
C is Element of the Points of IPP
{A,B,C} is Element of bool the Points of IPP
{a,b,C} is Element of bool the Points of IPP
O is Element of the Points of IPP
{q,C,O} is Element of bool the Points of IPP
{a,A,O} is Element of bool the Points of IPP
Q is Element of the Points of IPP
{q,Q} is Element of bool the Points of IPP
{b,O,Q} is Element of bool the Points of IPP
c10 is Element of the Points of IPP
{A,Q,c10} is Element of bool the Points of IPP
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Lines of IPP
O2 is Element of the Lines of IPP
O3 is Element of the Lines of IPP
o99 is Element of the Lines of IPP
oo9 is Element of the Lines of IPP
Q is Element of the Lines of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
{a,b,q} is Element of bool the Points of IPP
bool the Points of IPP is set
A is Element of the Points of IPP
B is Element of the Points of IPP
{A,B} is Element of bool the Points of IPP
C is Element of the Points of IPP
{A,C} is Element of bool the Points of IPP
{a,C,B} is Element of bool the Points of IPP
O is Element of the Points of IPP
{A,O} is Element of bool the Points of IPP
{q,B,O} is Element of bool the Points of IPP
{b,C,O} is Element of bool the Points of IPP
Q is Element of the Lines of IPP
c10 is Element of the Lines of IPP
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Lines of IPP
O2 is Element of the Lines of IPP
O3 is Element of the Lines of IPP
o99 is Element of the Lines of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
B is Element of the Points of IPP
{A,B} is Element of bool the Points of IPP
bool the Points of IPP is set
C is Element of the Points of IPP
O is Element of the Points of IPP
{B,C,O} is Element of bool the Points of IPP
{a,b,O} is Element of bool the Points of IPP
Q is Element of the Points of IPP
{A,O,Q} is Element of bool the Points of IPP
{a,B,Q} is Element of bool the Points of IPP
c10 is Element of the Points of IPP
{A,c10} is Element of bool the Points of IPP
{b,Q,c10} is Element of bool the Points of IPP
{B,c10,q} is Element of bool the Points of IPP
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Lines of IPP
O2 is Element of the Lines of IPP
O3 is Element of the Lines of IPP
o99 is Element of the Lines of IPP
oo9 is Element of the Lines of IPP
Q is Element of the Lines of IPP

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Lines of IPP
A is Element of the Lines of IPP
B is Element of the Lines of IPP
IncProj (q,a,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (B,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,a,B)) * (IncProj (B,b,A)) is Relation-like Function-like set
C is Element of the Lines of IPP
IncProj (C,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
O is Element of the Lines of IPP
Q is Element of the Points of IPP
c10 is Element of the Points of IPP
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Points of IPP
O2 is Element of the Points of IPP
O3 is Element of the Lines of IPP
o99 is Element of the Points of IPP
{b,c10,o9} is Element of bool the Points of IPP
bool the Points of IPP is set
{a,c10,O2} is Element of bool the Points of IPP
oo9 is Element of the Points of IPP
{oo9,O2,o9} is Element of bool the Points of IPP
{Q,O2} is Element of bool the Points of IPP
{Q,c10} is Element of bool the Points of IPP
{a,b,oo9} is Element of bool the Points of IPP
{Q,o9} is Element of bool the Points of IPP
IncProj (q,oo9,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,oo9,C)) * (IncProj (C,b,A)) is Relation-like Function-like set
Q is Element of the Points of IPP
IncProj (q,Q,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,Q,C)) * (IncProj (C,b,A)) is Relation-like Function-like set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Lines of IPP
A is Element of the Lines of IPP
B is Element of the Lines of IPP
IncProj (q,a,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (B,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,a,B)) * (IncProj (B,b,A)) is Relation-like Function-like set
C is Element of the Lines of IPP
IncProj (C,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
O is Element of the Lines of IPP
Q is Element of the Points of IPP
{a,b,Q} is Element of bool the Points of IPP
bool the Points of IPP is set
c10 is Element of the Points of IPP
Q is Element of the Lines of IPP
O1 is Element of the Points of IPP
{a,c10,O1} is Element of bool the Points of IPP
o9 is Element of the Points of IPP
{o9,c10} is Element of bool the Points of IPP
{o9,Q,O1} is Element of bool the Points of IPP
O2 is Element of the Lines of IPP
O3 is Element of the Points of IPP
{b,O1,O3} is Element of bool the Points of IPP
o99 is Element of the Points of IPP
oo9 is Element of the Lines of IPP
{c10,o99,Q} is Element of bool the Points of IPP
Q is Element of the Points of IPP
{c10,O3,Q} is Element of bool the Points of IPP
{o9,O3} is Element of bool the Points of IPP
IncProj (q,Q,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,Q,C)) * (IncProj (C,b,A)) is Relation-like Function-like set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Lines of IPP
A is Element of the Lines of IPP
B is Element of the Lines of IPP
IncProj (q,a,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (B,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,a,B)) * (IncProj (B,b,A)) is Relation-like Function-like set
C is Element of the Lines of IPP
IncProj (C,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
O is Element of the Lines of IPP
Q is Element of the Points of IPP
IncProj (q,Q,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,Q,C)) * (IncProj (C,b,A)) is Relation-like Function-like set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Lines of IPP
A is Element of the Lines of IPP
B is Element of the Lines of IPP
IncProj (q,a,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (B,b,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,a,B)) * (IncProj (B,b,A)) is Relation-like Function-like set
C is Element of the Lines of IPP
IncProj (q,a,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
O is Element of the Lines of IPP
IncProj (A,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (B,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
Q is Element of the Points of IPP
(IncProj (A,b,B)) * (IncProj (B,a,q)) is Relation-like Function-like set
IncProj (C,a,q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
Q is Element of the Points of IPP
IncProj (A,Q,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,Q,C)) * (IncProj (C,a,q)) is Relation-like Function-like set
IncProj (C,Q,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (q,a,C)) * (IncProj (C,Q,A)) is Relation-like Function-like set
(IncProj (A,b,B)) " is Relation-like Function-like set
(IncProj (q,a,B)) * ((IncProj (A,b,B)) ") is Relation-like Function-like set
(IncProj (B,a,q)) " is Relation-like Function-like set
((IncProj (B,a,q)) ") * ((IncProj (A,b,B)) ") is Relation-like Function-like set
((IncProj (A,Q,C)) * (IncProj (C,a,q))) " is Relation-like Function-like set
(IncProj (C,a,q)) " is Relation-like Function-like set
(IncProj (A,Q,C)) " is Relation-like Function-like set
((IncProj (C,a,q)) ") * ((IncProj (A,Q,C)) ") is Relation-like Function-like set
((IncProj (C,a,q)) ") * (IncProj (C,Q,A)) is Relation-like Function-like set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
B is Element of the Points of IPP
C is Element of the Points of IPP
O is Element of the Lines of IPP
Q is Element of the Lines of IPP
c10 is Element of the Lines of IPP
IncProj (O,a,c10) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (c10,b,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (O,a,c10)) * (IncProj (c10,b,Q)) is Relation-like Function-like set
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Lines of IPP
IncProj (O,b,o9) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (o9,a,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (O,b,o9)) * (IncProj (o9,a,Q)) is Relation-like Function-like set
(IPP,O) is Element of bool the Points of IPP
bool the Points of IPP is set
{ b1 where b1 is Element of the Points of IPP : b1 on O } is set
dom (IncProj (O,a,c10)) is Element of bool the Points of IPP
dom (IncProj (O,b,o9)) is Element of bool the Points of IPP
dom ((IncProj (O,b,o9)) * (IncProj (o9,a,Q))) is set
y is Element of the Points of IPP
((IncProj (O,a,c10)) * (IncProj (c10,b,Q))) . y is set
((IncProj (O,b,o9)) * (IncProj (o9,a,Q))) . y is set
(IncProj (O,a,c10)) . y is set
(IncProj (O,b,o9)) . y is set
x9 is Element of the Points of IPP
(IncProj (c10,b,Q)) . x9 is set
O1 is Element of the Lines of IPP
y is Element of the Points of IPP
O3 is Element of the Lines of IPP
x99 is Element of the Points of IPP
O2 is Element of the Lines of IPP
{y,B,C} is Element of bool the Points of IPP
{A,x99,C} is Element of bool the Points of IPP
{A,a,B} is Element of bool the Points of IPP
{q,b,C} is Element of bool the Points of IPP
{b,y,y} is Element of bool the Points of IPP
{b,x99,x9} is Element of bool the Points of IPP
{y,a,x9} is Element of bool the Points of IPP
{q,A,x9} is Element of bool the Points of IPP
{q,y,B} is Element of bool the Points of IPP
{x99,a,y} is Element of bool the Points of IPP
O4 is Element of the Lines of IPP
(IncProj (c10,b,Q)) . ((IncProj (O,a,c10)) . y) is set
(IncProj (o9,a,Q)) . ((IncProj (O,b,o9)) . y) is set
y is set
((IncProj (O,a,c10)) * (IncProj (c10,b,Q))) . y is set
((IncProj (O,b,o9)) * (IncProj (o9,a,Q))) . y is set
x9 is Element of the Points of IPP
dom ((IncProj (O,a,c10)) * (IncProj (c10,b,Q))) is set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
B is Element of the Lines of IPP
C is Element of the Lines of IPP
O is Element of the Lines of IPP
IncProj (B,a,O) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (O,b,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (B,a,O)) * (IncProj (O,b,C)) is Relation-like Function-like set
Q is Element of the Lines of IPP
c10 is Element of the Points of IPP
Q is Element of the Lines of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Points of IPP
O2 is Element of the Lines of IPP
O3 is Element of the Points of IPP
o99 is Element of the Lines of IPP
{a,b,A} is Element of bool the Points of IPP
bool the Points of IPP is set
{q,O3} is Element of bool the Points of IPP
{b,c10,O3} is Element of bool the Points of IPP
{a,c10,o9} is Element of bool the Points of IPP
{A,o9,O3} is Element of bool the Points of IPP
{q,o9} is Element of bool the Points of IPP
{q,c10} is Element of bool the Points of IPP
IncProj (B,A,o99) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (o99,b,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (B,A,o99)) * (IncProj (o99,b,C)) is Relation-like Function-like set
oo9 is Element of the Lines of IPP
IncProj (B,A,oo9) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (oo9,b,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (B,A,oo9)) * (IncProj (oo9,b,C)) is Relation-like Function-like set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Points of IPP
B is Element of the Lines of IPP
C is Element of the Lines of IPP
O is Element of the Lines of IPP
IncProj (B,a,O) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (O,b,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (B,a,O)) * (IncProj (O,b,C)) is Relation-like Function-like set
Q is Element of the Lines of IPP
c10 is Element of the Points of IPP
{a,b,c10} is Element of bool the Points of IPP
bool the Points of IPP is set
Q is Element of the Points of IPP
O1 is Element of the Lines of IPP
o9 is Element of the Points of IPP
{a,Q,o9} is Element of bool the Points of IPP
{q,c10,o9} is Element of bool the Points of IPP
O2 is Element of the Lines of IPP
{q,Q} is Element of bool the Points of IPP
O3 is Element of the Lines of IPP
o99 is Element of the Points of IPP
{Q,o99,c10} is Element of bool the Points of IPP
oo9 is Element of the Points of IPP
{b,o9,oo9} is Element of bool the Points of IPP
{Q,oo9,A} is Element of bool the Points of IPP
Q is Element of the Lines of IPP
{q,oo9} is Element of bool the Points of IPP
IncProj (B,A,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (Q,b,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (B,A,Q)) * (IncProj (Q,b,C)) is Relation-like Function-like set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Lines of IPP
B is Element of the Lines of IPP
C is Element of the Lines of IPP
IncProj (A,a,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (C,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,a,C)) * (IncProj (C,b,B)) is Relation-like Function-like set
O is Element of the Lines of IPP
Q is Element of the Points of IPP
c10 is Element of the Lines of IPP
IncProj (A,q,c10) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (c10,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,q,c10)) * (IncProj (c10,b,B)) is Relation-like Function-like set
Q is Element of the Lines of IPP
IncProj (A,q,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (Q,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,q,Q)) * (IncProj (Q,b,B)) is Relation-like Function-like set
c10 is Element of the Lines of IPP
IncProj (A,q,c10) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (c10,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,q,c10)) * (IncProj (c10,b,B)) is Relation-like Function-like set
Q is Element of the Lines of IPP
IncProj (A,q,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (Q,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,q,Q)) * (IncProj (Q,b,B)) is Relation-like Function-like set
c10 is Element of the Lines of IPP
IncProj (A,q,c10) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (c10,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,q,c10)) * (IncProj (c10,b,B)) is Relation-like Function-like set
Q is Element of the Lines of IPP
IncProj (A,q,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (Q,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,q,Q)) * (IncProj (Q,b,B)) is Relation-like Function-like set

the Points of IPP is V4() set
the Lines of IPP is V4() set
a is Element of the Points of IPP
b is Element of the Points of IPP
q is Element of the Points of IPP
A is Element of the Lines of IPP
B is Element of the Lines of IPP
C is Element of the Lines of IPP
IncProj (A,a,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
[: the Points of IPP, the Points of IPP:] is set
bool [: the Points of IPP, the Points of IPP:] is set
IncProj (C,b,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,a,C)) * (IncProj (C,b,B)) is Relation-like Function-like set
O is Element of the Lines of IPP
IncProj (C,a,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (B,b,C) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
Q is Element of the Points of IPP
(IncProj (B,b,C)) * (IncProj (C,a,A)) is Relation-like Function-like set
Q is Element of the Lines of IPP
IncProj (B,q,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (Q,a,A) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (B,q,Q)) * (IncProj (Q,a,A)) is Relation-like Function-like set
IncProj (A,a,Q) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
IncProj (Q,q,B) is Relation-like the Points of IPP -defined the Points of IPP -valued Function-like Element of bool [: the Points of IPP, the Points of IPP:]
(IncProj (A,a,Q)) * (IncProj (Q,q,B)) is Relation-like Function-like set
(IncProj (B,b,C)) " is Relation-like Function-like set
(IncProj (A,a,C)) * ((IncProj (B,b,C)) ") is Relation-like Function-like set
(IncProj (C,a,A)) " is Relation-like Function-like set
((IncProj (C,a,A)) ") * ((IncProj (B,b,C)) ") is Relation-like Function-like set
((IncProj (B,q,Q)) * (IncProj (Q,a,A))) " is Relation-like Function-like set
(IncProj (Q,a,A)) " is Relation-like Function-like set
(IncProj (B,q,Q)) " is Relation-like Function-like set
((IncProj (Q,a,A)) ") * ((IncProj (B,q,Q)) ") is Relation-like Function-like set
(IncProj (A,a,Q)) * ((IncProj (B,q,Q)) ") is Relation-like Function-like set