:: AFF_4 semantic presentation

K75() is Element of K24(K71())
K71() is set
K24(K71()) is set
K70() is set
K24(K70()) is set
K24(K75()) is set
{} is empty set
1 is non empty set
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
X is set
a is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
M is Element of the carrier of AS
M is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

N is set
r is Element of the carrier of AS
M is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

the Element of (AS,a,X) is Element of (AS,a,X)
N is Element of the carrier of AS
r is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

Y is set
N is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

N is set
r is Element of the carrier of AS
M is Element of the carrier of AS
M is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in Y )
}
is set

(AS,X,Y) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // X & b2 in Y )
}
is set

N is set
r is Element of the carrier of AS
M is Element of the carrier of AS
M is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
M is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
N9 is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
Line (Y,Y) is Element of K24( the carrier of AS)
P is Element of the carrier of AS
P is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
N9 is Element of the carrier of AS
Line (X,N9) is Element of K24( the carrier of AS)
A is Element of the carrier of AS
A is Element of the carrier of AS
N9 is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
(AS,Y,N) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // Y & b2 in N )
}
is set

(AS,X,N) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // X & b2 in N )
}
is set

r is set
N is Element of the carrier of AS
M is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
(AS,Y,N) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // Y & b2 in N )
}
is set

r is Element of K24( the carrier of AS)
M is set
M9 is Element of the carrier of AS
N9 is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
A is Element of the carrier of AS
P is Element of the carrier of AS
N is Element of the carrier of AS
M is Element of the carrier of AS
M is Element of the carrier of AS
P is Element of the carrier of AS
P is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Line (a,X) is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
(AS,r,M) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // r & b2 in M )
}
is set

AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in Y )
}
is set

N is set
r is Element of the carrier of AS
M is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in Y )
}
is set

N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // a & b2 in X )
}
is set

Y is Element of K24( the carrier of AS)
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of K24( the carrier of AS)
M9 is Element of the carrier of AS
N9 is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
(AS,N,r) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // N & b2 in r )
}
is set

(AS,N,Y) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // N & b2 in Y )
}
is set

M is Element of the carrier of AS
(AS,N,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // N & b2 in X )
}
is set

M is Element of the carrier of AS
N is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
(AS,r,M) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // r & b2 in M )
}
is set

(AS,r,Y) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // r & b2 in Y )
}
is set

N is Element of the carrier of AS
M9 is Element of the carrier of AS
N9 is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
Y /\ N is Element of K24( the carrier of AS)
Line (a,X) is Element of K24( the carrier of AS)
N is set
N9 is set
M9 is Element of the carrier of AS
Y is Element of the carrier of AS
Line (M9,Y) is Element of K24( the carrier of AS)
P is Element of the carrier of AS
Line (M9,P) is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
Line (M9,Y) is Element of K24( the carrier of AS)
P is Element of the carrier of AS
Line (M9,P) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
N /\ r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
X is Element of K24( the carrier of AS)
a is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
Line (a,X) is Element of K24( the carrier of AS)
(AS,Y,(Line (a,X))) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
(AS,X,Y) is Element of K24( the carrier of AS)
(AS,a,(AS,X,Y)) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
(AS,Y,N) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // Y & b2 in N )
}
is set

r is Element of the carrier of AS
M is Element of the carrier of AS
(AS,r,Y) is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
Line (Y,N) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
(AS,X,Y) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // X & b2 in Y )
}
is set

N is Element of the carrier of AS
r is Element of the carrier of AS
(AS,N,X) is Element of K24( the carrier of AS)
N is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of K24( the carrier of AS)
(AS,M,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // M & b2 in X )
}
is set

r is Element of K24( the carrier of AS)
(AS,r,X) is Element of K24( the carrier of AS)
{ b1 where b1 is Element of the carrier of AS : ex b2 being Element of the carrier of AS st
( b1,b2 // r & b2 in X )
}
is set

r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of the carrier of AS
Line (a,N) is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
(AS,Y,a) is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of K24( the carrier of AS)
(AS,Y,a) is Element of K24( the carrier of AS)
(AS,Y,N) is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
(AS,Y,a) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
(AS,N,r) is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
(AS,Y,a) is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
(AS,a,N) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
Line (X,Y) is Element of K24( the carrier of AS)
Line (N,r) is Element of K24( the carrier of AS)
M9 is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of K24( the carrier of AS)
N9 is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
A is Element of K24( the carrier of AS)
P is Element of K24( the carrier of AS)
Line (Y,N) is Element of K24( the carrier of AS)
Line (M,N) is Element of K24( the carrier of AS)
Line (X,Y) is Element of K24( the carrier of AS)
Line (r,M) is Element of K24( the carrier of AS)
Line (X,N) is Element of K24( the carrier of AS)
Line (r,N) is Element of K24( the carrier of AS)
y is Element of the carrier of AS
x is Element of the carrier of AS
K is Element of the carrier of AS
(AS,y,(Line (X,Y))) is Element of K24( the carrier of AS)
Line (K,x) is Element of K24( the carrier of AS)
Line (a,Y) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of K24( the carrier of AS)
N9 is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
A is Element of K24( the carrier of AS)
P is Element of the carrier of AS
M is Element of the carrier of AS
Line (a,P) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
N is Element of the carrier of AS
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of the carrier of AS
N9 is Element of the carrier of AS
Y is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
N9 is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
A is Element of K24( the carrier of AS)
Line (Y,r) is Element of K24( the carrier of AS)
Line (N,M) is Element of K24( the carrier of AS)
Line (a,Y) is Element of K24( the carrier of AS)
Line (X,N) is Element of K24( the carrier of AS)
Line (a,r) is Element of K24( the carrier of AS)
Line (X,M) is Element of K24( the carrier of AS)
p is Element of the carrier of AS
y is Element of the carrier of AS
x is Element of the carrier of AS
(AS,p,(Line (a,Y))) is Element of K24( the carrier of AS)
Line (x,y) is Element of K24( the carrier of AS)
(AS,Y,N) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
N9 is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
A is Element of the carrier of AS
(AS,A,N) is Element of K24( the carrier of AS)
M is Element of the carrier of AS
M is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M is Element of the carrier of AS
M is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M9 is Element of the carrier of AS
M is Element of the carrier of AS
N9 is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
K24( the carrier of AS) is set
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
N9 is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of K24( the carrier of AS)
Line (X,Y) is Element of K24( the carrier of AS)
Line (a,Y) is Element of K24( the carrier of AS)
(AS,N,(Line (a,Y))) is Element of K24( the carrier of AS)
(AS,r,(Line (X,Y))) is Element of K24( the carrier of AS)
A is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
K24( the carrier of AS) is set
M is Element of K24( the carrier of AS)
Line (a,N) is Element of K24( the carrier of AS)
Line (X,r) is Element of K24( the carrier of AS)
Line (a,X) is Element of K24( the carrier of AS)
Line (N,r) is Element of K24( the carrier of AS)
A is Element of K24( the carrier of AS)
(AS,Y,(Line (a,N))) is Element of K24( the carrier of AS)
Line (a,Y) is Element of K24( the carrier of AS)
M is Element of the carrier of AS
P is Element of the carrier of AS
Line (P,Y) is Element of K24( the carrier of AS)
Line (a,Y) is Element of K24( the carrier of AS)
N is Element of the carrier of AS
P is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
N is Element of the carrier of AS
M9 is Element of the carrier of AS
N9 is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
(AS,N9,Y) is Element of K24( the carrier of AS)
A is Element of the carrier of AS
(AS,A,Y) is Element of K24( the carrier of AS)
M is Element of the carrier of AS
N is Element of the carrier of AS
c9 is Element of the carrier of AS
Line (N,c9) is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of the carrier of AS
M9 is Element of the carrier of AS
Line (M,N) is Element of K24( the carrier of AS)
Line (M,M9) is Element of K24( the carrier of AS)
A is Element of K24( the carrier of AS)
(AS,Y,A) is Element of K24( the carrier of AS)
P is Element of K24( the carrier of AS)
(AS,Y,P) is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
M9 is Element of K24( the carrier of AS)
N9 is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of the carrier of AS
r is Element of the carrier of AS
M is Element of the carrier of AS
N is Element of K24( the carrier of AS)
(AS,M,a) is Element of K24( the carrier of AS)
(AS,N,X) is Element of K24( the carrier of AS)
(AS,M,(AS,N,X)) is Element of K24( the carrier of AS)
(AS,M,X) is Element of K24( the carrier of AS)
(AS,M,N) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
(AS,X,Y) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
the Element of X is Element of X
M is Element of the carrier of AS
N is Element of K24( the carrier of AS)
r is Element of the carrier of AS
(AS,r,N) is Element of K24( the carrier of AS)
(AS,M,(AS,r,N)) is Element of K24( the carrier of AS)
(AS,M,N) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of K24( the carrier of AS)
X is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
Line (Y,N) is Element of K24( the carrier of AS)
Line (Y,r) is Element of K24( the carrier of AS)
(AS,Y,(Line (Y,r))) is Element of K24( the carrier of AS)
(AS,Y,(Line (Y,N))) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
X is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
a is Element of the carrier of AS
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r /\ N is Element of K24( the carrier of AS)
M /\ N is Element of K24( the carrier of AS)
(AS,Y,(r /\ N)) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of K24( the carrier of AS)
M is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
r /\ N is Element of K24( the carrier of AS)
M /\ N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
Y is Element of the carrier of AS
N is Element of the carrier of AS
r is Element of the carrier of AS
Line (Y,N) is Element of K24( the carrier of AS)
Line (Y,r) is Element of K24( the carrier of AS)
(AS,a,(Line (Y,N))) is Element of K24( the carrier of AS)
(AS,a,(Line (Y,r))) is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
X is Element of K24( the carrier of AS)
a is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of the carrier of AS
Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
(AS,X,Y) is Element of K24( the carrier of AS)
(AS,a,(AS,X,Y)) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)
N is Element of K24( the carrier of AS)
(AS,a,N) is Element of K24( the carrier of AS)
AS is non empty V46() AffinSpace-like AffinStruct
the carrier of AS is non empty V5() set
K24( the carrier of AS) is set
a is Element of the carrier of AS
X is Element of K24( the carrier of AS)
(AS,a,X) is Element of K24( the carrier of AS)
Y is Element of K24( the carrier of AS)
(AS,a,Y) is Element of K24( the carrier of AS)