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

{ b

( b

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)

{ b

( b

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)

{ b

( b

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)

{ b

( b

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)

{ b

( b

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)

{ b

( b

(AS,X,Y) is Element of K24( the carrier of AS)

{ b

( b

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)

{ b

( b

(AS,X,N) is Element of K24( the carrier of AS)

{ b

( b

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)

{ b

( b

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)

{ b

( b

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)

{ b

( b

Y is Element of K24( the carrier of AS)

(AS,a,Y) is Element of K24( the carrier of AS)

{ b

( b

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)

{ b

( b

Y is Element of K24( the carrier of AS)

(AS,a,Y) is Element of K24( the carrier of AS)

{ b

( b

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)

{ b

( b

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)

{ b

( b

(AS,N,Y) is Element of K24( the carrier of AS)

{ b

( b

M is Element of the carrier of AS

(AS,N,X) is Element of K24( the carrier of AS)

{ b

( b

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)

{ b

( b

(AS,r,Y) is Element of K24( the carrier of AS)

{ b

( b

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)

{ b

( b

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)

{ b

( b

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)

{ b

( b

r is Element of K24( the carrier of AS)

(AS,r,X) is Element of K24( the carrier of AS)

{ b

( b

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)