:: 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