:: AFPROJ semantic presentation

K139() is Element of bool K135()
K135() is set
bool K135() is non empty set
K134() is set
bool K134() is non empty set
bool K139() is non empty set
{} is empty set
1 is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of the carrier of AS
b is Element of the carrier of AS
c is Element of the carrier of AS
Line (a,b) is Element of bool the carrier of AS
Line (a,c) is Element of bool the carrier of AS
Plane ((Line (a,c)),(Line (a,b))) is Element of bool the carrier of AS
c9 is set
L1 is Element of the carrier of AS
L1 * (Line (a,c)) is Element of bool the carrier of AS
R1 is Element of the carrier of AS
{ b₁ where b₁ is Element of the carrier of AS : ex b₂ being Element of the carrier of AS st
( b₁,b₂ // Line (a,c) & b₂ in Line (a,b) ) } is set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of bool the carrier of AS
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
the Element of c is Element of c
the Element of b is Element of b
b9 is Element of the carrier of AS
b9 * a is Element of bool the carrier of AS
b9 * XX is Element of bool the carrier of AS
b9 + b is Element of bool the carrier of AS
c9 is Element of the carrier of AS
c9 * a is Element of bool the carrier of AS
c9 * XX is Element of bool the carrier of AS
c9 + c is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of bool the carrier of AS
b is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
bool (bool the carrier of AS) is non empty set
a is set
b is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
bool (bool the carrier of AS) is non empty set
a is set
b is Element of bool the carrier of AS
a is non empty non trivial AffinSpace-like AffinStruct
the carrier of a is non empty non trivial set
bool the carrier of a is non empty set
XX is set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
b is set
c is Element of bool the carrier of a
(a) is Element of bool (bool the carrier of a)
bool (bool the carrier of a) is non empty set
{ b₁ where b₁ is Element of bool the carrier of a : b₁ is being_line } is set
a is non empty non trivial AffinSpace-like AffinStruct
the carrier of a is non empty non trivial set
bool the carrier of a is non empty set
XX is set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
b is set
c is Element of bool the carrier of a
(a) is Element of bool (bool the carrier of a)
bool (bool the carrier of a) is non empty set
{ b₁ where b₁ is Element of bool the carrier of a : b₁ is being_plane } is set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
[:(AS),(AS):] is Relation-like bool the carrier of AS -defined bool the carrier of AS -valued Element of bool [:(bool the carrier of AS),(bool the carrier of AS):]
[:(bool the carrier of AS),(bool the carrier of AS):] is non empty set
bool [:(bool the carrier of AS),(bool the carrier of AS):] is non empty set
c is set
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
[d,a9] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
d is set
a9 is Element of bool the carrier of AS
[d,d] is V1() set
{d,d} is non empty set
{d} is non empty set
{{d,d},{d}} is non empty set
c is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
field c is set
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
[d,a9] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
b9 is Element of bool the carrier of AS
c9 is Element of bool the carrier of AS
[b9,c9] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{b9,c9} is non empty set
{b9} is non empty set
{{b9,c9},{b9}} is non empty set
d is set
a9 is set
b9 is set
[d,a9] is V1() set
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
[a9,b9] is V1() set
{a9,b9} is non empty set
{a9} is non empty set
{{a9,b9},{a9}} is non empty set
c9 is Element of bool the carrier of AS
L1 is Element of bool the carrier of AS
Q1 is Element of bool the carrier of AS
[d,b9] is V1() set
{d,b9} is non empty set
{{d,b9},{d}} is non empty set
d is set
a9 is set
[d,a9] is V1() set
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
b9 is Element of bool the carrier of AS
c9 is Element of bool the carrier of AS
[a9,d] is V1() set
{a9,d} is non empty set
{a9} is non empty set
{{a9,d},{a9}} is non empty set
dom c is set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
[:(AS),(AS):] is Relation-like bool the carrier of AS -defined bool the carrier of AS -valued Element of bool [:(bool the carrier of AS),(bool the carrier of AS):]
[:(bool the carrier of AS),(bool the carrier of AS):] is non empty set
bool [:(bool the carrier of AS),(bool the carrier of AS):] is non empty set
c is set
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
[d,a9] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
d is set
a9 is Element of bool the carrier of AS
[d,d] is V1() set
{d,d} is non empty set
{d} is non empty set
{{d,d},{d}} is non empty set
c is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
field c is set
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
[d,a9] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
b9 is Element of bool the carrier of AS
c9 is Element of bool the carrier of AS
[b9,c9] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{b9,c9} is non empty set
{b9} is non empty set
{{b9,c9},{b9}} is non empty set
d is set
a9 is set
b9 is set
[d,a9] is V1() set
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
[a9,b9] is V1() set
{a9,b9} is non empty set
{a9} is non empty set
{{a9,b9},{a9}} is non empty set
c9 is Element of bool the carrier of AS
L1 is Element of bool the carrier of AS
Q1 is Element of bool the carrier of AS
[d,b9] is V1() set
{d,b9} is non empty set
{{d,b9},{d}} is non empty set
d is set
a9 is set
[d,a9] is V1() set
{d,a9} is non empty set
{d} is non empty set
{{d,a9},{d}} is non empty set
b9 is Element of bool the carrier of AS
c9 is Element of bool the carrier of AS
[a9,d] is V1() set
{a9,d} is non empty set
{a9} is non empty set
{{a9,d},{a9}} is non empty set
dom c is set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
XX is Element of bool the carrier of AS
Class ((AS),XX) is Element of bool (AS)
bool (AS) is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
XX is Element of bool the carrier of AS
Class ((AS),XX) is Element of bool (AS)
bool (AS) is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
bool (AS) is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class ((AS),XX) is Element of bool (AS)
a is set
[a,XX] is V1() set
{a,XX} is non empty set
{a} is non empty set
{{a,XX},{a}} is non empty set
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
[b,c] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
[:(bool the carrier of AS),(bool the carrier of AS):] is non empty set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
d is Element of bool the carrier of AS
b is Element of bool the carrier of AS
[b,XX] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{b,XX} is non empty set
{b} is non empty set
{{b,XX},{b}} is non empty set
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
bool (AS) is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class ((AS),XX) is Element of bool (AS)
a is set
[a,XX] is V1() set
{a,XX} is non empty set
{a} is non empty set
{{a,XX},{a}} is non empty set
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
[b,c] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
[:(bool the carrier of AS),(bool the carrier of AS):] is non empty set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
d is Element of bool the carrier of AS
b is Element of bool the carrier of AS
[b,XX] is V1() Element of [:(bool the carrier of AS),(bool the carrier of AS):]
{b,XX} is non empty set
{b} is non empty set
{{b,XX},{b}} is non empty set
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
bool (AS) is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class ((AS),XX) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
b is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
bool (AS) is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class ((AS),XX) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
bool (AS) is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class ((AS),XX) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
b is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
XX is Element of the carrier of AS
a is Element of the carrier of AS
Line (XX,a) is Element of bool the carrier of AS
Class ((AS),(Line (XX,a))) is Element of bool (AS)
bool (AS) is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the Element of the carrier of AS is Element of the carrier of AS
a is Element of bool the carrier of AS
Class ((AS),a) is Element of bool (AS)
bool (AS) is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
XX is set
bool (AS) is non empty set
a is Element of bool (AS)
b is set
Class ((AS),b) is Element of bool (AS)
c is Element of bool the carrier of AS
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
Class ((AS),b) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
XX is set
bool (AS) is non empty set
a is Element of bool (AS)
b is set
Class ((AS),b) is Element of bool (AS)
c is Element of bool the carrier of AS
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
Class ((AS),b) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
XX is set
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b) is Element of bool (AS)
a is Element of the carrier of AS
a * b is Element of bool the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
XX is Element of bool the carrier of AS
a is set
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c) is Element of bool (AS)
d is Element of the carrier of AS
a9 is Element of the carrier of AS
b9 is Element of bool the carrier of AS
{1} is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
[:(AS),{1}:] is set
XX is set
a is set
b is set
[a,b] is V1() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
c is Element of bool the carrier of AS
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of bool the carrier of AS
[b,1] is V1() set
{b,1} is non empty set
{b} is non empty set
{{b,1},{b}} is non empty set
2 is non empty set
{2} is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
XX is set
a is set
b is set
[a,b] is V1() set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c) is Element of bool (AS)
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
[(AS,d),2] is V1() set
{(AS,d),2} is non empty set
{(AS,d)} is non empty set
{{(AS,d),2},{(AS,d)}} is non empty set
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
Class ((AS),b) is Element of bool (AS)
[(AS,b),2] is V1() set
{(AS,b),2} is non empty set
{(AS,b)} is non empty set
{{(AS,b),2},{(AS,b)}} is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
b is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
c is set
d is set
[c,d] is V1() set
{c,d} is non empty set
{c} is non empty set
{{c,d},{c}} is non empty set
a9 is Element of bool the carrier of AS
[a9,1] is V1() set
{a9,1} is non empty set
{a9} is non empty set
{{a9,1},{a9}} is non empty set
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
a9 is Element of bool the carrier of AS
b9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
[(AS,b9),2] is V1() set
{(AS,b9),2} is non empty set
{(AS,b9)} is non empty set
{{(AS,b9),2},{(AS,b9)}} is non empty set
a9 is Element of bool the carrier of AS
[a9,1] is V1() set
{a9,1} is non empty set
{a9} is non empty set
{{a9,1},{a9}} is non empty set
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
b9 is Element of bool the carrier of AS
c9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
Class ((AS),b9) is Element of bool (AS)
(AS,c9) is Element of bool (AS)
Class ((AS),c9) is Element of bool (AS)
[(AS,c9),2] is V1() set
{(AS,c9),2} is non empty set
{(AS,c9)} is non empty set
{{(AS,c9),2},{(AS,c9)}} is non empty set
a9 is Element of bool the carrier of AS
[a9,1] is V1() set
{a9,1} is non empty set
{a9} is non empty set
{{a9,1},{a9}} is non empty set
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
b9 is Element of bool the carrier of AS
c9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
Class ((AS),b9) is Element of bool (AS)
(AS,c9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c9) is Element of bool (AS)
[(AS,c9),2] is V1() set
{(AS,c9),2} is non empty set
{(AS,c9)} is non empty set
{{(AS,c9),2},{(AS,c9)}} is non empty set
XX is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
a is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
b is set
c is set
[b,c] is V1() set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
b9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
[(AS,b9),2] is V1() set
{(AS,b9),2} is non empty set
{(AS,b9)} is non empty set
{{(AS,b9),2},{(AS,b9)}} is non empty set
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
b9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
[(AS,b9),2] is V1() set
{(AS,b9),2} is non empty set
{(AS,b9)} is non empty set
{{(AS,b9),2},{(AS,b9)}} is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
b is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
c is set
d is set
[c,d] is V1() set
{c,d} is non empty set
{c} is non empty set
{{c,d},{c}} is non empty set
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
b9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
b9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
b9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
XX is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
a is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
b is set
c is set
[b,c] is V1() set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
XX is set
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
Class ((AS),b) is Element of bool (AS)
a is non empty non trivial AffinSpace-like AffinStruct
the carrier of a is non empty non trivial set
bool the carrier of a is non empty set
XX is set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
b is set
c is Element of bool the carrier of a
(a,c) is Element of bool (a)
(a) is Element of bool (bool the carrier of a)
bool (bool the carrier of a) is non empty set
{ b₁ where b₁ is Element of bool the carrier of a : b₁ is being_line } is set
bool (a) is non empty set
(a) is Relation-like (a) -defined (a) -valued symmetric transitive V28((a)) Element of bool [:(a),(a):]
[:(a),(a):] is set
bool [:(a),(a):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of a : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class ((a),c) is Element of bool (a)
(a) is strict IncProjStr
(a) is non empty set
Class (a) is a_partition of (a)
(a) is non empty set
(a) is Element of bool (bool the carrier of a)
{ b₁ where b₁ is Element of bool the carrier of a : b₁ is being_plane } is set
(a) is Relation-like (a) -defined (a) -valued symmetric transitive V28((a)) Element of bool [:(a),(a):]
[:(a),(a):] is set
bool [:(a),(a):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of a : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (a) is a_partition of (a)
(a) is Relation-like (a) -defined (a) -valued Element of bool [:(a),(a):]
[:(a),(a):] is non empty set
bool [:(a),(a):] is non empty set
IncProjStr(# (a),(a),(a) #) is strict IncProjStr
the Points of (a) is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
XX is set
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
XX is set
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
Class ((AS),b) is Element of bool (AS)
[(AS,b),2] is V1() set
{(AS,b),2} is non empty set
{(AS,b)} is non empty set
{{(AS,b),2},{(AS,b)}} is non empty set
c is Element of bool the carrier of AS
[c,1] is V1() set
{c,1} is non empty set
{c} is non empty set
{{c,1},{c}} is non empty set
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
[(AS,d),2] is V1() set
{(AS,d),2} is non empty set
{(AS,d)} is non empty set
{{(AS,d),2},{(AS,d)}} is non empty set
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
Class ((AS),b) is Element of bool (AS)
[(AS,b),2] is V1() set
{(AS,b),2} is non empty set
{(AS,b)} is non empty set
{{(AS,b),2},{(AS,b)}} is non empty set
c is Element of bool the carrier of AS
[c,1] is V1() set
{c,1} is non empty set
{c} is non empty set
{{c,1},{c}} is non empty set
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
[(AS,d),2] is V1() set
{(AS,d),2} is non empty set
{(AS,d)} is non empty set
{{(AS,d),2},{(AS,d)}} is non empty set
a is non empty non trivial AffinSpace-like AffinStruct
the carrier of a is non empty non trivial set
bool the carrier of a is non empty set
XX is set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
b is set
c is Element of bool the carrier of a
(a,c) is Element of bool (a)
(a) is Element of bool (bool the carrier of a)
bool (bool the carrier of a) is non empty set
{ b₁ where b₁ is Element of bool the carrier of a : b₁ is being_plane } is set
bool (a) is non empty set
(a) is Relation-like (a) -defined (a) -valued symmetric transitive V28((a)) Element of bool [:(a),(a):]
[:(a),(a):] is set
bool [:(a),(a):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of a : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class ((a),c) is Element of bool (a)
(a) is strict IncProjStr
(a) is non empty set
(a) is Element of bool (bool the carrier of a)
{ b₁ where b₁ is Element of bool the carrier of a : b₁ is being_line } is set
(a) is Relation-like (a) -defined (a) -valued symmetric transitive V28((a)) Element of bool [:(a),(a):]
[:(a),(a):] is set
bool [:(a),(a):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of a : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (a) is a_partition of (a)
(a) is non empty set
Class (a) is a_partition of (a)
(a) is Relation-like (a) -defined (a) -valued Element of bool [:(a),(a):]
[:(a),(a):] is non empty set
bool [:(a),(a):] is non empty set
IncProjStr(# (a),(a),(a) #) is strict IncProjStr
the Lines of (a) is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
XX is set
[XX,2] is V1() set
{XX,2} is non empty set
{XX} is non empty set
{{XX,2},{XX}} is non empty set
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the carrier of AS
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of the Points of (AS)
c is Element of the Lines of (AS)
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
the carrier of AS /\ (AS) is set
[d,1] `1 is set
[b,c] is V1() Element of [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
bool [: the Points of (AS), the Lines of (AS):] is non empty set
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
[(AS,a9),2] is V1() set
{(AS,a9),2} is non empty set
{(AS,a9)} is non empty set
{{(AS,a9),2},{(AS,a9)}} is non empty set
[XX,[a,1]] is V1() set
{XX,[a,1]} is non empty set
{XX} is non empty set
{{XX,[a,1]},{XX}} is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the carrier of AS
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
b is Element of the Points of (AS)
c is Element of the Lines of (AS)
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
[d,1] `2 is set
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
[(AS,a9),2] is V1() set
{(AS,a9),2} is non empty set
{(AS,a9)} is non empty set
{{(AS,a9),2},{(AS,a9)}} is non empty set
the carrier of AS /\ (AS) is set
[b,c] is V1() Element of [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
bool [: the Points of (AS), the Lines of (AS):] is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of the Points of (AS)
c is Element of the Lines of (AS)
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
the carrier of AS /\ (AS) is set
[b,c] is V1() Element of [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
bool [: the Points of (AS), the Lines of (AS):] is non empty set
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
[(AS,a9),2] is V1() set
{(AS,a9),2} is non empty set
{(AS,a9)} is non empty set
{{(AS,a9),2},{(AS,a9)}} is non empty set
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
b is Element of the Points of (AS)
c is Element of the Lines of (AS)
d is Element of bool the carrier of AS
a9 is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
[(AS,a9),2] is V1() set
{(AS,a9),2} is non empty set
{(AS,a9)} is non empty set
{{(AS,a9),2},{(AS,a9)}} is non empty set
b9 is Element of bool the carrier of AS
c9 is Element of bool the carrier of AS
[b,c] is V1() Element of [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
bool [: the Points of (AS), the Lines of (AS):] is non empty set
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
[(AS,XX),[(AS,a),2]] is V1() set
{(AS,XX),[(AS,a),2]} is non empty set
{(AS,XX)} is non empty set
{{(AS,XX),[(AS,a),2]},{(AS,XX)}} is non empty set
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
[XX,1] is V1() set
{XX,1} is non empty set
{XX} is non empty set
{{XX,1},{XX}} is non empty set
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
b is Element of the Points of (AS)
c is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
[(AS,XX),2] is V1() set
{(AS,XX),2} is non empty set
{(AS,XX)} is non empty set
{{(AS,XX),2},{(AS,XX)}} is non empty set
a is Element of bool the carrier of AS
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b) is Element of bool (AS)
c is Element of the Points of (AS)
d is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
b is Element of the Lines of (AS)
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
[(AS,XX),2] is V1() set
{(AS,XX),2} is non empty set
{(AS,XX)} is non empty set
{{(AS,XX),2},{(AS,XX)}} is non empty set
a is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
[XX,1] is V1() set
{XX,1} is non empty set
{XX} is non empty set
{{XX,1},{XX}} is non empty set
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
Class ((AS),c) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
[XX,1] is V1() set
{XX,1} is non empty set
{XX} is non empty set
{{XX,1},{XX}} is non empty set
a is Element of the Points of (AS)
b is Element of the Points of (AS)
c is Element of the Lines of (AS)
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
(AS,XX) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),XX) is Element of bool (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
b is Element of the Points of (AS)
c is Element of the Lines of (AS)
[b,c] is V1() Element of [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
{b,c} is non empty set
{b} is non empty set
{{b,c},{b}} is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
bool [: the Points of (AS), the Lines of (AS):] is non empty set
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
[b,2] is V1() set
{b,2} is non empty set
{b} is non empty set
{{b,2},{b}} is non empty set
c is Element of the Lines of (AS)
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
c is Element of the Lines of (AS)
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
a9 is Element of bool the carrier of AS
(AS,a9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a9) is Element of bool (AS)
b9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
Class ((AS),b9) is Element of bool (AS)
c9 is Element of bool the carrier of AS
(AS,c9) is Element of bool (AS)
Class ((AS),c9) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
the Points of (AS) is non empty set
XX is Element of the Lines of (AS)
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
b is Element of the carrier of AS
c is Element of the carrier of AS
d is Element of the carrier of AS
Line (c,d) is Element of bool the carrier of AS
Line (b,d) is Element of bool the carrier of AS
Line (b,c) is Element of bool the carrier of AS
(AS,(Line (b,c))) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),(Line (b,c))) is Element of bool (AS)
(AS,(Line (c,d))) is Element of bool (AS)
Class ((AS),(Line (c,d))) is Element of bool (AS)
(AS,(Line (b,d))) is Element of bool (AS)
Class ((AS),(Line (b,d))) is Element of bool (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
c9 is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b) is Element of bool (AS)
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
Class ((AS),c) is Element of bool (AS)
d is Element of the carrier of AS
a9 is Element of the carrier of AS
d * b is Element of bool the carrier of AS
b9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
c9 is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
the Element of the carrier of AS is Element of the carrier of AS
a is Element of bool the carrier of AS
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
c is Element of the carrier of AS
Line ( the Element of the carrier of AS,c) is Element of bool the carrier of AS
(AS,(Line ( the Element of the carrier of AS,c))) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),(Line ( the Element of the carrier of AS,c))) is Element of bool (AS)
a9 is Element of the Points of (AS)
b is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
c is Element of the Lines of (AS)
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
[(AS,d),2] is V1() set
{(AS,d),2} is non empty set
{(AS,d)} is non empty set
{{(AS,d),2},{(AS,d)}} is non empty set
a9 is Element of bool the carrier of AS
[a9,1] is V1() set
{a9,1} is non empty set
{a9} is non empty set
{{a9,1},{a9}} is non empty set
(AS,a9) is Element of bool (AS)
Class ((AS),a9) is Element of bool (AS)
[(AS,a9),2] is V1() set
{(AS,a9),2} is non empty set
{(AS,a9)} is non empty set
{{(AS,a9),2},{(AS,a9)}} is non empty set
b9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
c9 is Element of bool the carrier of AS
(AS,c9) is Element of bool (AS)
Class ((AS),c9) is Element of bool (AS)
L1 is Element of bool the carrier of AS
[L1,1] is V1() set
{L1,1} is non empty set
{L1} is non empty set
{{L1,1},{L1}} is non empty set
Q1 is Element of the Lines of (AS)
c9 is Element of the carrier of AS
b9 is Element of the carrier of AS
c9 is Element of bool the carrier of AS
(AS,c9) is Element of bool (AS)
Class ((AS),c9) is Element of bool (AS)
c9 is Element of the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
the Points of (AS) is non empty set
XX is Element of the Lines of (AS)
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
b is Element of the carrier of AS
c is Element of the carrier of AS
d is Element of the carrier of AS
Line (c,d) is Element of bool the carrier of AS
Line (b,d) is Element of bool the carrier of AS
Line (b,c) is Element of bool the carrier of AS
(AS,(Line (b,c))) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),(Line (b,c))) is Element of bool (AS)
(AS,(Line (c,d))) is Element of bool (AS)
Class ((AS),(Line (c,d))) is Element of bool (AS)
(AS,(Line (b,d))) is Element of bool (AS)
Class ((AS),(Line (b,d))) is Element of bool (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
c9 is Element of the Points of (AS)
L1 is Element of the Points of (AS)
Q1 is Element of the Points of (AS)
R1 is Element of the Points of (AS)
(AS,a) is Element of bool (AS)
Class ((AS),a) is Element of bool (AS)
c is Element of the carrier of AS
d is Element of the carrier of AS
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
b is Element of the Points of (AS)
c9 is Element of the Points of (AS)
L1 is Element of the Points of (AS)
Q1 is Element of the Points of (AS)
the carrier of AS /\ (AS) is set
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
c9 is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of bool the carrier of AS
(AS,b) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b) is Element of bool (AS)
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
Class ((AS),c) is Element of bool (AS)
d is Element of the carrier of AS
a9 is Element of the carrier of AS
d * b is Element of bool the carrier of AS
b9 is Element of bool the carrier of AS
(AS,b9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b9) is Element of bool (AS)
[(AS,b9),2] is V1() set
{(AS,b9),2} is non empty set
{(AS,b9)} is non empty set
{{(AS,b9),2},{(AS,b9)}} is non empty set
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
c is Element of the carrier of AS
c * b is Element of bool the carrier of AS
[(c * b),1] is V1() set
{(c * b),1} is non empty set
{(c * b)} is non empty set
{{(c * b),1},{(c * b)}} is non empty set
d is Element of the Lines of (AS)
a9 is Element of the Lines of (AS)
c is Element of the Lines of (AS)
d is Element of the Lines of (AS)
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
Class ((AS),c) is Element of bool (AS)
b is Element of the carrier of AS
b * c is Element of bool the carrier of AS
[(b * c),1] is V1() set
{(b * c),1} is non empty set
{(b * c)} is non empty set
{{(b * c),1},{(b * c)}} is non empty set
d is Element of the Lines of (AS)
a9 is Element of the Lines of (AS)
c is Element of the carrier of AS
d is Element of bool the carrier of AS
[d,1] is V1() set
{d,1} is non empty set
{d} is non empty set
{{d,1},{d}} is non empty set
a9 is Element of the Lines of (AS)
b9 is Element of the Lines of (AS)
c is Element of the Lines of (AS)
d is Element of the Lines of (AS)
b is Element of the Lines of (AS)
c is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
the Points of (AS) is non empty set
XX is Element of the Lines of (AS)
a is Element of the Lines of (AS)
b is Element of bool the carrier of AS
[b,1] is V1() set
{b,1} is non empty set
{b} is non empty set
{{b,1},{b}} is non empty set
(AS,b) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b) is Element of bool (AS)
[(AS,b),2] is V1() set
{(AS,b),2} is non empty set
{(AS,b)} is non empty set
{{(AS,b),2},{(AS,b)}} is non empty set
c is Element of bool the carrier of AS
[c,1] is V1() set
{c,1} is non empty set
{c} is non empty set
{{c,1},{c}} is non empty set
(AS,c) is Element of bool (AS)
Class ((AS),c) is Element of bool (AS)
[(AS,c),2] is V1() set
{(AS,c),2} is non empty set
{(AS,c)} is non empty set
{{(AS,c),2},{(AS,c)}} is non empty set
(AS,b) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),b) is Element of bool (AS)
(AS,c) is Element of bool (AS)
Class ((AS),c) is Element of bool (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
d is Element of the carrier of AS
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
c9 is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the carrier of AS
a is Element of the carrier of AS
b is Element of the carrier of AS
Line (a,b) is Element of bool the carrier of AS
[(Line (a,b)),1] is V1() set
{(Line (a,b)),1} is non empty set
{(Line (a,b))} is non empty set
{{(Line (a,b)),1},{(Line (a,b))}} is non empty set
d is Element of the Points of (AS)
c is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
the Points of (AS) is non empty set
[: the Points of (AS), the Lines of (AS):] is non empty set
bool [: the Points of (AS), the Lines of (AS):] is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
[XX,b] is V1() Element of [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
{XX,b} is non empty set
{XX} is non empty set
{{XX,b},{XX}} is non empty set
[a,b] is V1() Element of [: the Points of (AS), the Lines of (AS):]
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
d is Element of the Points of (AS)
a9 is Element of the Lines of (AS)
[a9,2] is V1() set
{a9,2} is non empty set
{a9} is non empty set
{{a9,2},{a9}} is non empty set
c9 is Element of bool the carrier of AS
(AS,c9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c9) is Element of bool (AS)
L1 is Element of bool the carrier of AS
(AS,L1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),L1) is Element of bool (AS)
b9 is Element of the Lines of (AS)
Q1 is Element of bool the carrier of AS
(AS,Q1) is Element of bool (AS)
Class ((AS),Q1) is Element of bool (AS)
c is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
(AS) is strict IncProjStr
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
the Lines of (AS) is non empty set
[: the Points of (AS), the Lines of (AS):] is non empty set
bool [: the Points of (AS), the Lines of (AS):] is non empty set
the Points of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Lines of (AS)
[a,2] is V1() set
{a,2} is non empty set
{a} is non empty set
{{a,2},{a}} is non empty set
[XX,[a,2]] is V1() set
{XX,[a,2]} is non empty set
{XX} is non empty set
{{XX,[a,2]},{XX}} is non empty set
c is Element of the carrier of AS
b is Element of the Lines of (AS)
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
[XX,1] is V1() set
{XX,1} is non empty set
{XX} is non empty set
{{XX,1},{XX}} is non empty set
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
[c,1] is V1() set
{c,1} is non empty set
{c} is non empty set
{{c,1},{c}} is non empty set
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Lines of (AS)
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
R1 is Element of bool the carrier of AS
(AS,R1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),R1) is Element of bool (AS)
Q1 is Element of the carrier of AS
Q1 * a is Element of bool the carrier of AS
R1 is Element of the carrier of AS
Line (Q1,R1) is Element of bool the carrier of AS
Q1 is Element of bool the carrier of AS
(AS,Q1) is Element of bool (AS)
Class ((AS),Q1) is Element of bool (AS)
R1 is Element of the carrier of AS
R1 * XX is Element of bool the carrier of AS
R1 is Element of bool the carrier of AS
(AS,R1) is Element of bool (AS)
Class ((AS),R1) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of bool the carrier of AS
[XX,1] is V1() set
{XX,1} is non empty set
{XX} is non empty set
{{XX,1},{XX}} is non empty set
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c) is Element of bool (AS)
[(AS,c),2] is V1() set
{(AS,c),2} is non empty set
{(AS,c)} is non empty set
{{(AS,c),2},{(AS,c)}} is non empty set
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Lines of (AS)
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
Q1 is Element of bool the carrier of AS
(AS,Q1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),Q1) is Element of bool (AS)
Q1 is Element of bool the carrier of AS
(AS,Q1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),Q1) is Element of bool (AS)
R1 is Element of bool the carrier of AS
(AS,R1) is Element of bool (AS)
Class ((AS),R1) is Element of bool (AS)
R1 is Element of bool the carrier of AS
(AS,R1) is Element of bool (AS)
Class ((AS),R1) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
the Points of (AS) is non empty set
XX is Element of bool the carrier of AS
a is Element of bool the carrier of AS
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
b is Element of bool the carrier of AS
[b,1] is V1() set
{b,1} is non empty set
{b} is non empty set
{{b,1},{b}} is non empty set
c is Element of the Lines of (AS)
d is Element of the Lines of (AS)
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
a9 is Element of the Points of (AS)
(AS,b) is Element of bool (AS)
Class ((AS),b) is Element of bool (AS)
b9 is Element of the Points of (AS)
a9 is Element of the carrier of AS
b9 is Element of the Points of (AS)
c9 is Element of the Points of (AS)
a9 is Element of the Points of (AS)
b9 is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Lines of (AS)
b9 is Element of the Lines of (AS)
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
R1 is Element of bool the carrier of AS
[R1,1] is V1() set
{R1,1} is non empty set
{R1} is non empty set
{{R1,1},{R1}} is non empty set
(AS,R1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),R1) is Element of bool (AS)
[(AS,R1),2] is V1() set
{(AS,R1),2} is non empty set
{(AS,R1)} is non empty set
{{(AS,R1),2},{(AS,R1)}} is non empty set
S1 is Element of bool the carrier of AS
[S1,1] is V1() set
{S1,1} is non empty set
{S1} is non empty set
{{S1,1},{S1}} is non empty set
(AS,S1) is Element of bool (AS)
Class ((AS),S1) is Element of bool (AS)
[(AS,S1),2] is V1() set
{(AS,S1),2} is non empty set
{(AS,S1)} is non empty set
{{(AS,S1),2},{(AS,S1)}} is non empty set
A1 is Element of bool the carrier of AS
[A1,1] is V1() set
{A1,1} is non empty set
{A1} is non empty set
{{A1,1},{A1}} is non empty set
(AS,A1) is Element of bool (AS)
Class ((AS),A1) is Element of bool (AS)
[(AS,A1),2] is V1() set
{(AS,A1),2} is non empty set
{(AS,A1)} is non empty set
{{(AS,A1),2},{(AS,A1)}} is non empty set
B1 is Element of bool the carrier of AS
[B1,1] is V1() set
{B1,1} is non empty set
{B1} is non empty set
{{B1,1},{B1}} is non empty set
(AS,B1) is Element of bool (AS)
Class ((AS),B1) is Element of bool (AS)
[(AS,B1),2] is V1() set
{(AS,B1),2} is non empty set
{(AS,B1)} is non empty set
{{(AS,B1),2},{(AS,B1)}} is non empty set
Q1 is Element of the carrier of AS
p is Element of bool the carrier of AS
(AS,S1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),S1) is Element of bool (AS)
q is Element of the Points of (AS)
r is Element of the Points of (AS)
q is Element of the Points of (AS)
r is Element of the Points of (AS)
s is Element of the Points of (AS)
Y is Element of the Points of (AS)
q is Element of the Points of (AS)
r is Element of the Points of (AS)
(AS,A1) is Element of bool (AS)
Class ((AS),A1) is Element of bool (AS)
q is Element of the Points of (AS)
r is Element of the Points of (AS)
q is Element of the Points of (AS)
r is Element of the Points of (AS)
q is Element of the Points of (AS)
r is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Lines of (AS)
b9 is Element of the Lines of (AS)
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
R1 is Element of bool the carrier of AS
[R1,1] is V1() set
{R1,1} is non empty set
{R1} is non empty set
{{R1,1},{R1}} is non empty set
(AS,R1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),R1) is Element of bool (AS)
[(AS,R1),2] is V1() set
{(AS,R1),2} is non empty set
{(AS,R1)} is non empty set
{{(AS,R1),2},{(AS,R1)}} is non empty set
Q1 is Element of the carrier of AS
S1 is Element of bool the carrier of AS
[S1,1] is V1() set
{S1,1} is non empty set
{S1} is non empty set
{{S1,1},{S1}} is non empty set
(AS,S1) is Element of bool (AS)
Class ((AS),S1) is Element of bool (AS)
[(AS,S1),2] is V1() set
{(AS,S1),2} is non empty set
{(AS,S1)} is non empty set
{{(AS,S1),2},{(AS,S1)}} is non empty set
A1 is Element of bool the carrier of AS
[A1,1] is V1() set
{A1,1} is non empty set
{A1} is non empty set
{{A1,1},{A1}} is non empty set
(AS,A1) is Element of bool (AS)
Class ((AS),A1) is Element of bool (AS)
[(AS,A1),2] is V1() set
{(AS,A1),2} is non empty set
{(AS,A1)} is non empty set
{{(AS,A1),2},{(AS,A1)}} is non empty set
B1 is Element of the carrier of AS
p is Element of bool the carrier of AS
(AS,p) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),p) is Element of bool (AS)
q is Element of bool the carrier of AS
[q,1] is V1() set
{q,1} is non empty set
{q} is non empty set
{{q,1},{q}} is non empty set
(AS,q) is Element of bool (AS)
Class ((AS),q) is Element of bool (AS)
[(AS,q),2] is V1() set
{(AS,q),2} is non empty set
{(AS,q)} is non empty set
{{(AS,q),2},{(AS,q)}} is non empty set
r is Element of bool the carrier of AS
(AS,S1) is Element of bool (AS)
Class ((AS),S1) is Element of bool (AS)
s is Element of the carrier of AS
s * R1 is Element of bool the carrier of AS
Y is Element of bool the carrier of AS
(AS,Y) is Element of bool (AS)
Class ((AS),Y) is Element of bool (AS)
Y is Element of the carrier of AS
Line (B1,Y) is Element of bool the carrier of AS
(AS,A1) is Element of bool (AS)
Class ((AS),A1) is Element of bool (AS)
(AS,q) is Element of bool (AS)
Class ((AS),q) is Element of bool (AS)
s is Element of the Points of (AS)
Y is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Lines of (AS)
b9 is Element of the Lines of (AS)
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
Q1 is Element of the Points of (AS)
Q1 is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Lines of (AS)
b9 is Element of the Lines of (AS)
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
the Element of the carrier of AS is Element of the carrier of AS
R1 is Element of bool the carrier of AS
(AS,R1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),R1) is Element of bool (AS)
S1 is Element of bool the carrier of AS
(AS,S1) is Element of bool (AS)
Class ((AS),S1) is Element of bool (AS)
A1 is Element of bool the carrier of AS
(AS,A1) is Element of bool (AS)
Class ((AS),A1) is Element of bool (AS)
B1 is Element of bool the carrier of AS
(AS,B1) is Element of bool (AS)
Class ((AS),B1) is Element of bool (AS)
p is Element of bool the carrier of AS
(AS,p) is Element of bool (AS)
Class ((AS),p) is Element of bool (AS)
the Element of the carrier of AS * R1 is Element of bool the carrier of AS
the Element of the carrier of AS * A1 is Element of bool the carrier of AS
the Element of the carrier of AS * S1 is Element of bool the carrier of AS
the Element of the carrier of AS * B1 is Element of bool the carrier of AS
the Element of the carrier of AS * p is Element of bool the carrier of AS
C39 is Element of the carrier of AS
s is Element of the carrier of AS
C39 * ( the Element of the carrier of AS * p) is Element of bool the carrier of AS
s * ( the Element of the carrier of AS * p) is Element of bool the carrier of AS
A2 is Element of bool the carrier of AS
A3 is Element of bool the carrier of AS
B1 is Element of bool the carrier of AS
(AS,B1) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),B1) is Element of bool (AS)
[(AS,B1),2] is V1() set
{(AS,B1),2} is non empty set
{(AS,B1)} is non empty set
{{(AS,B1),2},{(AS,B1)}} is non empty set
B2 is Element of the Lines of (AS)
B2 is Element of bool the carrier of AS
(AS,B2) is Element of bool (AS)
Class ((AS),B2) is Element of bool (AS)
[(AS,B2),2] is V1() set
{(AS,B2),2} is non empty set
{(AS,B2)} is non empty set
{{(AS,B2),2},{(AS,B2)}} is non empty set
B3 is Element of the Lines of (AS)
B3 is Element of the carrier of AS
t is Element of the carrier of AS
Line (C39,s) is Element of bool the carrier of AS
Line (B3,t) is Element of bool the carrier of AS
(AS,( the Element of the carrier of AS * R1)) is Element of bool (AS)
Class ((AS),( the Element of the carrier of AS * R1)) is Element of bool (AS)
(AS,(C39 * ( the Element of the carrier of AS * p))) is Element of bool (AS)
Class ((AS),(C39 * ( the Element of the carrier of AS * p))) is Element of bool (AS)
(AS,( the Element of the carrier of AS * p)) is Element of bool (AS)
Class ((AS),( the Element of the carrier of AS * p)) is Element of bool (AS)
(AS,( the Element of the carrier of AS * A1)) is Element of bool (AS)
Class ((AS),( the Element of the carrier of AS * A1)) is Element of bool (AS)
(AS,( the Element of the carrier of AS * B1)) is Element of bool (AS)
Class ((AS),( the Element of the carrier of AS * B1)) is Element of bool (AS)
(AS,( the Element of the carrier of AS * S1)) is Element of bool (AS)
Class ((AS),( the Element of the carrier of AS * S1)) is Element of bool (AS)
y is Element of bool the carrier of AS
(AS,A3) is Element of bool (AS)
Class ((AS),A3) is Element of bool (AS)
[(AS,A3),2] is V1() set
{(AS,A3),2} is non empty set
{(AS,A3)} is non empty set
{{(AS,A3),2},{(AS,A3)}} is non empty set
(AS,A2) is Element of bool (AS)
Class ((AS),A2) is Element of bool (AS)
[(AS,A2),2] is V1() set
{(AS,A2),2} is non empty set
{(AS,A2)} is non empty set
{{(AS,A2),2},{(AS,A2)}} is non empty set
Z9 is Element of the Lines of (AS)
X is Element of the Lines of (AS)
(AS,(Line (C39,s))) is Element of bool (AS)
Class ((AS),(Line (C39,s))) is Element of bool (AS)
(AS,(Line (B3,t))) is Element of bool (AS)
Class ((AS),(Line (B3,t))) is Element of bool (AS)
Z9 is Element of the Points of (AS)
c₃₇ is Element of the Points of (AS)
X is Element of the Points of (AS)
Z9 is Element of the carrier of AS
Line ( the Element of the carrier of AS,Z9) is Element of bool the carrier of AS
(AS,(Line ( the Element of the carrier of AS,Z9))) is Element of bool (AS)
Class ((AS),(Line ( the Element of the carrier of AS,Z9))) is Element of bool (AS)
c₃₇ is Element of the Points of (AS)
q is Element of the Points of (AS)
Z9 is Element of the Points of (AS)
X is Element of the Points of (AS)
Q1 is Element of the Points of (AS)
Q1 is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
XX is Element of the Points of (AS)
a is Element of the Points of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a9 is Element of the Lines of (AS)
b9 is Element of the Lines of (AS)
c9 is Element of the Lines of (AS)
L1 is Element of the Lines of (AS)
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
[a9,2] is V1() set
{a9,2} is non empty set
{a9} is non empty set
{{a9,2},{a9}} is non empty set
[b9,2] is V1() set
{b9,2} is non empty set
{b9} is non empty set
{{b9,2},{b9}} is non empty set
[c9,2] is V1() set
{c9,2} is non empty set
{c9} is non empty set
{{c9,2},{c9}} is non empty set
[L1,2] is V1() set
{L1,2} is non empty set
{L1} is non empty set
{{L1,2},{L1}} is non empty set
the Points of (AS) is non empty set
p is Element of the Points of (AS)
Q1 is Element of the Lines of (AS)
R1 is Element of the Lines of (AS)
[b9,2] `1 is set
r is Element of the Points of (AS)
q is Element of the Points of (AS)
S1 is Element of the Lines of (AS)
B1 is Element of the Points of (AS)
s is Element of the Points of (AS)
A1 is Element of the Lines of (AS)
Y is Element of the Points of (AS)
[Y,[c9,2]] is V1() set
{Y,[c9,2]} is non empty set
{Y} is non empty set
{{Y,[c9,2]},{Y}} is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
bool [: the Points of (AS), the Lines of (AS):] is non empty set
C1 is Element of the Points of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
a is Element of the Points of (AS)
b is Element of the Points of (AS)
a is Element of the Lines of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a is Element of the Points of (AS)
c9 is Element of the Lines of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
L1 is Element of the Lines of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
Q1 is Element of the Lines of (AS)
R1 is Element of the Lines of (AS)
a is Element of the Points of (AS)
c is Element of the Lines of (AS)
b is Element of the Points of (AS)
d is Element of the Lines of (AS)
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
the non empty non trivial AffinSpace-like 2-dimensional AffinStruct is non empty non trivial AffinSpace-like 2-dimensional AffinStruct
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is strict linear partial up-2-dimensional up-3-rank Vebleian IncProjStr
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct is non empty non trivial set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is Element of bool (bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )
bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct is non empty set
bool (bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct : b<sub>1</sub> is being_line } is set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is Relation-like ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) -defined ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) -valued symmetric transitive V28(( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )) Element of bool [:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):]
[:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):] is set
bool [:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is a_partition of ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )
the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct \/ ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
[:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),{1}:] is set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is Element of bool (bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct : b<sub>1</sub> is being_plane } is set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is Relation-like ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) -defined ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) -valued symmetric transitive V28(( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )) Element of bool [:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):]
[:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):] is set
bool [:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of the non empty non trivial AffinSpace-like 2-dimensional AffinStruct : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is a_partition of ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )
[:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),{2}:] is non empty set
[:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),{1}:] \/ [:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),{2}:] is non empty set
( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is Relation-like ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) -defined ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) -valued Element of bool [:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):]
[:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):] is non empty set
bool [:( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ):] is non empty set
IncProjStr(# ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ),( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) #) is strict IncProjStr
the Lines of ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
the Points of ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct ) is non empty set
a is Element of the Lines of ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )
b is Element of the Lines of ( the non empty non trivial AffinSpace-like 2-dimensional AffinStruct )
AS is non empty non trivial AffinSpace-like 2-dimensional AffinStruct
(AS) is strict linear partial up-2-dimensional up-3-rank Vebleian IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Lines of (AS) is non empty set
the Points of (AS) is non empty set
a is Element of the Lines of (AS)
b is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict linear partial up-2-dimensional up-3-rank Vebleian IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Element of the carrier of AS is Element of the carrier of AS
a is Element of bool the carrier of AS
b is Element of the carrier of AS
Line ( the Element of the carrier of AS,b) is Element of bool the carrier of AS
the Lines of (AS) is non empty set
(AS,a) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),a) is Element of bool (AS)
[(AS,a),2] is V1() set
{(AS,a),2} is non empty set
{(AS,a)} is non empty set
{{(AS,a),2},{(AS,a)}} is non empty set
[(Line ( the Element of the carrier of AS,b)),1] is V1() set
{(Line ( the Element of the carrier of AS,b)),1} is non empty set
{(Line ( the Element of the carrier of AS,b))} is non empty set
{{(Line ( the Element of the carrier of AS,b)),1},{(Line ( the Element of the carrier of AS,b))}} is non empty set
the Points of (AS) is non empty set
d is Element of the Lines of (AS)
a9 is Element of the Lines of (AS)
b9 is Element of the Points of (AS)
c9 is Element of bool the carrier of AS
(AS,c9) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c9) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
a is Element of the Points of (AS)
b is Element of the Points of (AS)
a is Element of the Lines of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
d is Element of the Points of (AS)
a is Element of the Points of (AS)
c9 is Element of the Lines of (AS)
b is Element of the Points of (AS)
c is Element of the Points of (AS)
L1 is Element of the Lines of (AS)
d is Element of the Points of (AS)
a9 is Element of the Points of (AS)
Q1 is Element of the Lines of (AS)
R1 is Element of the Lines of (AS)
a is Element of the Points of (AS)
c is Element of the Lines of (AS)
b is Element of the Points of (AS)
d is Element of the Lines of (AS)
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict IncProjStr
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
a is Element of the Points of (AS)
b is Element of the Lines of (AS)
c is Element of bool the carrier of AS
(AS,c) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),c) is Element of bool (AS)
d is Element of bool the carrier of AS
(AS,d) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),d) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of bool the carrier of AS
b is Element of the carrier of AS
d is Element of the carrier of AS
c9 is Element of the carrier of AS
L1 is Element of the carrier of AS
a9 is Element of the carrier of AS
b9 is Element of the carrier of AS
c is Element of the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict linear partial up-2-dimensional up-3-rank Vebleian IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_line & b<sub>2</sub> is being_line & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of AS : b<sub>1</sub> is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of AS : ( b<sub>1</sub> is being_plane & b<sub>2</sub> is being_plane & b<sub>1</sub> '||' b<sub>2</sub> ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
a is Element of bool the carrier of AS
b is Element of bool the carrier of AS
c is Element of the carrier of AS
d is Element of the carrier of AS
c9 is Element of the carrier of AS
a9 is Element of the carrier of AS
L1 is Element of the carrier of AS
b9 is Element of the carrier of AS
Q1 is Element of the carrier of AS
Line (a9,Q1) is Element of bool the carrier of AS
Line (b9,c9) is Element of bool the carrier of AS
Line (a9,c9) is Element of bool the carrier of AS
Line (b9,L1) is Element of bool the carrier of AS
the Lines of (AS) is non empty set
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
[b,1] is V1() set
{b,1} is non empty set
{b} is non empty set
{{b,1},{b}} is non empty set
the Points of (AS) is non empty set
A1 is Element of the Points of (AS)
R1 is Element of the Lines of (AS)
Line (d,L1) is Element of bool the carrier of AS
(AS,(Line (a9,Q1))) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),(Line (a9,Q1))) is Element of bool (AS)
(AS,(Line (d,L1))) is Element of bool (AS)
Class ((AS),(Line (d,L1))) is Element of bool (AS)
r is Element of the Points of (AS)
Line (d,Q1) is Element of bool the carrier of AS
[(Line (a9,Q1)),1] is V1() set
{(Line (a9,Q1)),1} is non empty set
{(Line (a9,Q1))} is non empty set
{{(Line (a9,Q1)),1},{(Line (a9,Q1))}} is non empty set
[(Line (a9,c9)),1] is V1() set
{(Line (a9,c9)),1} is non empty set
{(Line (a9,c9))} is non empty set
{{(Line (a9,c9)),1},{(Line (a9,c9))}} is non empty set
[(Line (d,L1)),1] is V1() set
{(Line (d,L1)),1} is non empty set
{(Line (d,L1))} is non empty set
{{(Line (d,L1)),1},{(Line (d,L1))}} is non empty set
[(Line (b9,L1)),1] is V1() set
{(Line (b9,L1)),1} is non empty set
{(Line (b9,L1))} is non empty set
{{(Line (b9,L1)),1},{(Line (b9,L1))}} is non empty set
[(Line (b9,c9)),1] is V1() set
{(Line (b9,c9)),1} is non empty set
{(Line (b9,c9))} is non empty set
{{(Line (b9,c9)),1},{(Line (b9,c9))}} is non empty set
[(Line (d,Q1)),1] is V1() set
{(Line (d,Q1)),1} is non empty set
{(Line (d,Q1))} is non empty set
{{(Line (d,Q1)),1},{(Line (d,Q1))}} is non empty set
C39 is Element of the Points of (AS)
A1 is Element of the Lines of (AS)
Y is Element of the Points of (AS)
s is Element of the Points of (AS)
B2 is Element of bool the carrier of AS
(AS,B2) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),B2) is Element of bool (AS)
[(AS,B2),2] is V1() set
{(AS,B2),2} is non empty set
{(AS,B2)} is non empty set
{{(AS,B2),2},{(AS,B2)}} is non empty set
C1 is Element of the Points of (AS)
B3 is Element of the Lines of (AS)
B1 is Element of the Points of (AS)
S1 is Element of the Lines of (AS)
q is Element of the Points of (AS)
A3 is Element of the Lines of (AS)
A2 is Element of the Lines of (AS)
p is Element of the Points of (AS)
B1 is Element of the Lines of (AS)
s is Element of the Lines of (AS)
r is Element of the Lines of (AS)
[b,1] `1 is set
t is Element of the Points of (AS)
{p,r,t} is non empty Element of bool the Points of (AS)
bool the Points of (AS) is non empty set
{B1,Y,C39} is non empty Element of bool the Points of (AS)
{q,r,C39} is non empty Element of bool the Points of (AS)
{B1,p,q} is non empty Element of bool the Points of (AS)
{r,s,Y} is non empty Element of bool the Points of (AS)
{q,s,C1} is non empty Element of bool the Points of (AS)
{p,Y,C1} is non empty Element of bool the Points of (AS)
{C1,C39} is non empty Element of bool the Points of (AS)
{B1,s,t} is non empty Element of bool the Points of (AS)
O is Element of bool the carrier of AS
(AS,O) is Element of bool (AS)
Class ((AS),O) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
the carrier of AS is non empty non trivial set
bool the carrier of AS is non empty set
XX is Element of bool the carrier of AS
a is Element of bool the carrier of AS
b is Element of bool the carrier of AS
c is Element of the carrier of AS
d is Element of the carrier of AS
a9 is Element of the carrier of AS
b9 is Element of the carrier of AS
L1 is Element of the carrier of AS
Q1 is Element of the carrier of AS
c9 is Element of the carrier of AS
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict linear partial up-2-dimensional up-3-rank Vebleian IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
a is Element of bool the carrier of AS
b is Element of bool the carrier of AS
c is Element of bool the carrier of AS
d is Element of the carrier of AS
a9 is Element of the carrier of AS
b9 is Element of the carrier of AS
c9 is Element of the carrier of AS
L1 is Element of the carrier of AS
Q1 is Element of the carrier of AS
R1 is Element of the carrier of AS
the Points of (AS) is non empty set
the Lines of (AS) is non empty set
[a,1] is V1() set
{a,1} is non empty set
{a} is non empty set
{{a,1},{a}} is non empty set
[b,1] is V1() set
{b,1} is non empty set
{b} is non empty set
{{b,1},{b}} is non empty set
[c,1] is V1() set
{c,1} is non empty set
{c} is non empty set
{{c,1},{c}} is non empty set
Line (L1,R1) is Element of bool the carrier of AS
Line (Q1,R1) is Element of bool the carrier of AS
Line (b9,c9) is Element of bool the carrier of AS
Line (a9,c9) is Element of bool the carrier of AS
Line (a9,b9) is Element of bool the carrier of AS
(AS,(Line (a9,b9))) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),(Line (a9,b9))) is Element of bool (AS)
(AS,(Line (a9,c9))) is Element of bool (AS)
Class ((AS),(Line (a9,c9))) is Element of bool (AS)
S1 is Element of the Points of (AS)
C1 is Element of the Lines of (AS)
Line (L1,Q1) is Element of bool the carrier of AS
[(Line (b9,c9)),1] is V1() set
{(Line (b9,c9)),1} is non empty set
{(Line (b9,c9))} is non empty set
{{(Line (b9,c9)),1},{(Line (b9,c9))}} is non empty set
[(Line (a9,c9)),1] is V1() set
{(Line (a9,c9)),1} is non empty set
{(Line (a9,c9))} is non empty set
{{(Line (a9,c9)),1},{(Line (a9,c9))}} is non empty set
[(Line (a9,b9)),1] is V1() set
{(Line (a9,b9)),1} is non empty set
{(Line (a9,b9))} is non empty set
{{(Line (a9,b9)),1},{(Line (a9,b9))}} is non empty set
[(Line (Q1,R1)),1] is V1() set
{(Line (Q1,R1)),1} is non empty set
{(Line (Q1,R1))} is non empty set
{{(Line (Q1,R1)),1},{(Line (Q1,R1))}} is non empty set
[(Line (L1,R1)),1] is V1() set
{(Line (L1,R1)),1} is non empty set
{(Line (L1,R1))} is non empty set
{{(Line (L1,R1)),1},{(Line (L1,R1))}} is non empty set
[(Line (L1,Q1)),1] is V1() set
{(Line (L1,Q1)),1} is non empty set
{(Line (L1,Q1))} is non empty set
{{(Line (L1,Q1)),1},{(Line (L1,Q1))}} is non empty set
r is Element of the Points of (AS)
A2 is Element of the Lines of (AS)
r is Element of the Points of (AS)
A1 is Element of the Lines of (AS)
s is Element of the Points of (AS)
B2 is Element of the Lines of (AS)
B1 is Element of the Points of (AS)
{B1,r,s} is non empty Element of bool the Points of (AS)
bool the Points of (AS) is non empty set
Y is Element of the Lines of (AS)
C39 is Element of the Lines of (AS)
q is Element of the Points of (AS)
B3 is Element of the Lines of (AS)
s is Element of the Points of (AS)
{B1,s,q} is non empty Element of bool the Points of (AS)
[c,1] `1 is set
[b,1] `1 is set
A1 is Element of the Points of (AS)
{S1,r,s} is non empty Element of bool the Points of (AS)
{S1,B1,A1} is non empty Element of bool the Points of (AS)
{r,r,A1} is non empty Element of bool the Points of (AS)
B1 is Element of the Lines of (AS)
p is Element of the Points of (AS)
{S1,p,q} is non empty Element of bool the Points of (AS)
t is Element of the Points of (AS)
{r,p,t} is non empty Element of bool the Points of (AS)
{t,q,s} is non empty Element of bool the Points of (AS)
A3 is Element of the Lines of (AS)
{p,s,A1} is non empty Element of bool the Points of (AS)
{r,s,t} is non empty Element of bool the Points of (AS)
O is Element of the Lines of (AS)
(AS) is strict IncProjStr
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
the Points of (AS) is non empty set
y is Element of the Points of (AS)
[y,O] is V1() Element of [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
{y,O} is non empty set
{y} is non empty set
{{y,O},{y}} is non empty set
the Inc of (AS) is Relation-like the Points of (AS) -defined the Lines of (AS) -valued Element of bool [: the Points of (AS), the Lines of (AS):]
[: the Points of (AS), the Lines of (AS):] is non empty set
bool [: the Points of (AS), the Lines of (AS):] is non empty set
Y is Element of the Points of (AS)
[Y,O] is V1() Element of [: the Points of (AS), the Lines of (AS):]
{Y,O} is non empty set
{Y} is non empty set
{{Y,O},{Y}} is non empty set
the Lines of (AS) is non empty set
Z9 is Element of the Lines of (AS)
[Z9,2] is V1() set
{Z9,2} is non empty set
{Z9} is non empty set
{{Z9,2},{Z9}} is non empty set
X is Element of bool the carrier of AS
(AS,X) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),X) is Element of bool (AS)
[(AS,X),2] is V1() set
{(AS,X),2} is non empty set
{(AS,X)} is non empty set
{{(AS,X),2},{(AS,X)}} is non empty set
Y is Element of bool the carrier of AS
(AS,Y) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),Y) is Element of bool (AS)
[(AS,Y),2] is V1() set
{(AS,Y),2} is non empty set
{(AS,Y)} is non empty set
{{(AS,Y),2},{(AS,Y)}} is non empty set
Y is Element of bool the carrier of AS
(AS,Y) is Element of bool (AS)
Class ((AS),Y) is Element of bool (AS)
AS is non empty non trivial AffinSpace-like AffinStruct
(AS) is strict linear partial up-2-dimensional up-3-rank Vebleian IncProjStr
(AS) is non empty set
the carrier of AS is non empty non trivial set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
bool the carrier of AS is non empty set
bool (bool the carrier of AS) is non empty set
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_line } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_line & b₂ is being_line & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
the carrier of AS \/ (AS) is non empty set
(AS) is non empty set
[:(AS),{1}:] is set
(AS) is non empty set
(AS) is Element of bool (bool the carrier of AS)
{ b₁ where b₁ is Element of bool the carrier of AS : b₁ is being_plane } is set
(AS) is Relation-like (AS) -defined (AS) -valued symmetric transitive V28((AS)) Element of bool [:(AS),(AS):]
[:(AS),(AS):] is set
bool [:(AS),(AS):] is non empty set
{ [b₁,b₂] where b₁, b₂ is Element of bool the carrier of AS : ( b₁ is being_plane & b₂ is being_plane & b₁ '||' b₂ ) } is set
Class (AS) is a_partition of (AS)
[:(AS),{2}:] is non empty set
[:(AS),{1}:] \/ [:(AS),{2}:] is non empty set
(AS) is Relation-like (AS) -defined (AS) -valued Element of bool [:(AS),(AS):]
[:(AS),(AS):] is non empty set
bool [:(AS),(AS):] is non empty set
IncProjStr(# (AS),(AS),(AS) #) is strict IncProjStr
a is Element of the carrier of AS
b is Element of the carrier of AS
c is Element of the carrier of AS
d is Element of the carrier of AS
Line (a,d) is Element of bool the carrier of AS
Line (b,d) is Element of bool the carrier of AS
Line (c,d) is Element of bool the carrier of AS
Line (a,c) is Element of bool the carrier of AS
Line (a,b) is Element of bool the carrier of AS
the Points of (AS) is non empty set
(AS,(Line (a,b))) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),(Line (a,b))) is Element of bool (AS)
(AS,(Line (a,c))) is Element of bool (AS)
Class ((AS),(Line (a,c))) is Element of bool (AS)
(AS,(Line (a,d))) is Element of bool (AS)
Class ((AS),(Line (a,d))) is Element of bool (AS)
Line (b,c) is Element of bool the carrier of AS
the Lines of (AS) is non empty set
[(Line (a,b)),1] is V1() set
{(Line (a,b)),1} is non empty set
{(Line (a,b))} is non empty set
{{(Line (a,b)),1},{(Line (a,b))}} is non empty set
[(Line (c,d)),1] is V1() set
{(Line (c,d)),1} is non empty set
{(Line (c,d))} is non empty set
{{(Line (c,d)),1},{(Line (c,d))}} is non empty set
[(Line (b,d)),1] is V1() set
{(Line (b,d)),1} is non empty set
{(Line (b,d))} is non empty set
{{(Line (b,d)),1},{(Line (b,d))}} is non empty set
[(Line (a,c)),1] is V1() set
{(Line (a,c)),1} is non empty set
{(Line (a,c))} is non empty set
{{(Line (a,c)),1},{(Line (a,c))}} is non empty set
[(Line (a,d)),1] is V1() set
{(Line (a,d)),1} is non empty set
{(Line (a,d))} is non empty set
{{(Line (a,d)),1},{(Line (a,d))}} is non empty set
[(Line (b,c)),1] is V1() set
{(Line (b,c)),1} is non empty set
{(Line (b,c))} is non empty set
{{(Line (b,c)),1},{(Line (b,c))}} is non empty set
a9 is Element of the Points of (AS)
L1 is Element of the Lines of (AS)
r is Element of the Points of (AS)
B1 is Element of the Lines of (AS)
s is Element of the Points of (AS)
c9 is Element of the Points of (AS)
{c9,r,s} is non empty Element of bool the Points of (AS)
bool the Points of (AS) is non empty set
q is Element of the Points of (AS)
R1 is Element of the Lines of (AS)
S1 is Element of the Lines of (AS)
b9 is Element of the Points of (AS)
p is Element of the Points of (AS)
{b9,p,r} is non empty Element of bool the Points of (AS)
{b9,q,s} is non empty Element of bool the Points of (AS)
Y is Element of bool the carrier of AS
(AS,Y) is Element of bool (AS)
bool (AS) is non empty set
Class ((AS),Y) is Element of bool (AS)
[(AS,Y),2] is V1() set
{(AS,Y),2} is non empty set
{(AS,Y)} is non empty set
{{(AS,Y),2},{(AS,Y)}} is non empty set
C1 is Element of the Lines of (AS)
Q1 is Element of the Lines of (AS)
A1 is Element of the Lines of (AS)
{c9,p,q} is non empty Element of bool the Points of (AS)
{a9,b9} is non empty Element of bool the Points of (AS)
{a9,q,r} is non empty Element of bool the Points of (AS)
b * (Line (a,c)) is Element of bool the carrier of AS
{a9,p,s} is non empty Element of bool the Points of (AS)