:: DIRAF semantic presentation

K100() is Element of bool K96()

K96() is set

bool K96() is non empty set

K95() is set

bool K95() is non empty set

bool K100() is non empty set

{} is empty set

1 is non empty set

S is non empty set

[:S,S:] is non empty set

[:[:S,S:],[:S,S:]:] is non empty set

bool [:[:S,S:],[:S,S:]:] is non empty set

AS is V7() V10([:S,S:]) V11([:S,S:]) Element of bool [:[:S,S:],[:S,S:]:]

y is V7() V10([:S,S:]) V11([:S,S:]) Element of bool [:[:S,S:],[:S,S:]:]

z is Element of S

t is Element of S

[z,t] is Element of [:S,S:]

x9 is Element of S

y9 is Element of S

[x9,y9] is Element of [:S,S:]

[[z,t],[x9,y9]] is Element of [:[:S,S:],[:S,S:]:]

[y9,x9] is Element of [:S,S:]

[[z,t],[y9,x9]] is Element of [:[:S,S:],[:S,S:]:]

z9 is Element of S

t9 is Element of S

[z9,t9] is Element of [:S,S:]

u9 is Element of S

u is Element of S

[u9,u] is Element of [:S,S:]

[[z9,t9],[u9,u]] is Element of [:[:S,S:],[:S,S:]:]

[u,u9] is Element of [:S,S:]

[[z9,t9],[u,u9]] is Element of [:[:S,S:],[:S,S:]:]

y is V7() V10([:S,S:]) V11([:S,S:]) Element of bool [:[:S,S:],[:S,S:]:]

z is V7() V10([:S,S:]) V11([:S,S:]) Element of bool [:[:S,S:],[:S,S:]:]

t is set

x9 is set

[t,x9] is set

y9 is Element of S

z9 is Element of S

[y9,z9] is Element of [:S,S:]

[z9,y9] is Element of [:S,S:]

[t,[z9,y9]] is set

t9 is Element of S

u9 is Element of S

[t9,u9] is Element of [:S,S:]

t9 is Element of S

u9 is Element of S

[t9,u9] is Element of [:S,S:]

y9 is Element of S

z9 is Element of S

[y9,z9] is Element of [:S,S:]

[z9,y9] is Element of [:S,S:]

[t,[z9,y9]] is set

t9 is Element of S

u9 is Element of S

[t9,u9] is Element of [:S,S:]

t9 is Element of S

u9 is Element of S

[t9,u9] is Element of [:S,S:]

S is non empty AffinStruct

the carrier of S is non empty set

the CONGR of S is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

( the carrier of S, the CONGR of S) is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

AffinStruct(# the carrier of S,( the carrier of S, the CONGR of S) #) is strict AffinStruct

S is non empty AffinStruct

(S) is strict AffinStruct

the carrier of S is non empty set

the CONGR of S is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

( the carrier of S, the CONGR of S) is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

AffinStruct(# the carrier of S,( the carrier of S, the CONGR of S) #) is strict AffinStruct

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty AffinStruct

the carrier of S is non empty set

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty AffinStruct

the carrier of S is non empty set

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

[: the carrier of S, the carrier of S:] is non empty set

the CONGR of S is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

( the carrier of S, the CONGR of S) is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

AS is Element of the carrier of S

x is Element of the carrier of S

[AS,x] is Element of [: the carrier of S, the carrier of S:]

y is Element of the carrier of S

z is Element of the carrier of S

[y,z] is Element of [: the carrier of S, the carrier of S:]

[[AS,x],[y,z]] is Element of [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[z,y] is Element of [: the carrier of S, the carrier of S:]

[[AS,x],[z,y]] is Element of [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[z,y] is Element of [: the carrier of S, the carrier of S:]

[[AS,x],[z,y]] is Element of [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of S

y9 is Element of the carrier of S

z9 is Element of the carrier of S

t9 is Element of the carrier of S

u9 is Element of the carrier of S

t is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of S

S is non empty AffinStruct

the carrier of S is non empty set

S is non empty AffinStruct

the carrier of S is non empty set

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

S is non empty non trivial OAffinSpace-like AffinStruct

(S) is non empty strict AffinStruct

the carrier of S is non empty non trivial set

the CONGR of S is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

( the carrier of S, the CONGR of S) is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

AffinStruct(# the carrier of S,( the carrier of S, the CONGR of S) #) is strict AffinStruct

AS is non empty AffinStruct

the carrier of AS is non empty set

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of AS

y9 is Element of the carrier of AS

z9 is Element of the carrier of AS

t9 is Element of the carrier of AS

[: the carrier of AS, the carrier of AS:] is non empty set

[x9,y9] is Element of [: the carrier of AS, the carrier of AS:]

[z9,t9] is Element of [: the carrier of AS, the carrier of AS:]

[[x9,y9],[z9,t9]] is Element of [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:]

[:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:] is non empty set

the CONGR of AS is V7() V10([: the carrier of AS, the carrier of AS:]) V11([: the carrier of AS, the carrier of AS:]) Element of bool [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:]

bool [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:] is non empty set

[x,y] is Element of [: the carrier of S, the carrier of S:]

[z,t] is Element of [: the carrier of S, the carrier of S:]

[[x,y],[z,t]] is Element of [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[t,z] is Element of [: the carrier of S, the carrier of S:]

[[x,y],[t,z]] is Element of [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[x,y] is Element of [: the carrier of S, the carrier of S:]

[z,t] is Element of [: the carrier of S, the carrier of S:]

[[x,y],[z,t]] is Element of [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[t,z] is Element of [: the carrier of S, the carrier of S:]

[[x,y],[t,z]] is Element of [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[: the carrier of AS, the carrier of AS:] is non empty set

[x9,y9] is Element of [: the carrier of AS, the carrier of AS:]

[z9,t9] is Element of [: the carrier of AS, the carrier of AS:]

[[x9,y9],[z9,t9]] is Element of [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:]

[:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:] is non empty set

the CONGR of AS is V7() V10([: the carrier of AS, the carrier of AS:]) V11([: the carrier of AS, the carrier of AS:]) Element of bool [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:]

bool [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:] is non empty set

S is non empty non trivial OAffinSpace-like AffinStruct

(S) is non empty strict AffinStruct

the carrier of S is non empty non trivial set

the CONGR of S is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

( the carrier of S, the CONGR of S) is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

AffinStruct(# the carrier of S,( the carrier of S, the CONGR of S) #) is strict AffinStruct

AS is non empty AffinStruct

the carrier of AS is non empty set

x is Element of the carrier of AS

y is Element of the carrier of AS

z is Element of the carrier of AS

t is Element of the carrier of AS

x9 is Element of the carrier of AS

y9 is Element of the carrier of AS

z9 is Element of the carrier of S

t9 is Element of the carrier of S

u9 is Element of the carrier of S

u is Element of the carrier of S

u9 is Element of the carrier of S

w9 is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of AS

x9 is Element of the carrier of AS

y9 is Element of the carrier of AS

x is Element of the carrier of AS

z is Element of the carrier of AS

y is Element of the carrier of AS

t is Element of the carrier of S

y9 is Element of the carrier of S

x9 is Element of the carrier of S

z9 is Element of the carrier of S

t9 is Element of the carrier of AS

x is Element of the carrier of AS

y is Element of the carrier of AS

z is Element of the carrier of AS

t is Element of the carrier of S

x9 is Element of the carrier of S

y9 is Element of the carrier of S

z9 is Element of the carrier of S

t9 is Element of the carrier of AS

z is Element of the carrier of AS

x is Element of the carrier of AS

t is Element of the carrier of AS

y is Element of the carrier of AS

z9 is Element of the carrier of S

x9 is Element of the carrier of S

t9 is Element of the carrier of S

y9 is Element of the carrier of S

u9 is Element of the carrier of S

u is Element of the carrier of AS

the non empty non trivial OAffinSpace-like AffinStruct is non empty non trivial OAffinSpace-like AffinStruct

( the non empty non trivial OAffinSpace-like AffinStruct ) is non empty strict AffinStruct

the carrier of the non empty non trivial OAffinSpace-like AffinStruct is non empty non trivial set

the CONGR of the non empty non trivial OAffinSpace-like AffinStruct is V7() V10([: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]) V11([: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]) Element of bool [:[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]:]

[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :] is non empty set

[:[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]:] is non empty set

bool [:[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]:] is non empty set

( the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the CONGR of the non empty non trivial OAffinSpace-like AffinStruct ) is V7() V10([: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]) V11([: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]) Element of bool [:[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the carrier of the non empty non trivial OAffinSpace-like AffinStruct :]:]

AffinStruct(# the carrier of the non empty non trivial OAffinSpace-like AffinStruct ,( the carrier of the non empty non trivial OAffinSpace-like AffinStruct , the CONGR of the non empty non trivial OAffinSpace-like AffinStruct ) #) is strict AffinStruct

the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct ) is non empty set

AS is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

y is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

x is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

z is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

t is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

x9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

y is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

AS is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

z is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

x is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

AS is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

x is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

y is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

z is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

t is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

x9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

y9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

z9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

t9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

u9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

u is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

u9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

w9 is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

c

AS is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

x is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

y is Element of the carrier of ( the non empty non trivial OAffinSpace-like AffinStruct )

AS is non empty non trivial () AffinStruct

the carrier of AS is non empty non trivial set

z is non empty non trivial () AffinStruct

the carrier of z is non empty non trivial set

z9 is non empty non trivial () AffinStruct

the carrier of z9 is non empty non trivial set

c

the carrier of c

c

the carrier of c

c

the carrier of c

c

the carrier of c

S is non empty non trivial () AffinStruct

the carrier of S is non empty non trivial set

x is Element of the carrier of AS

y is Element of the carrier of AS

t is Element of the carrier of z

x9 is Element of the carrier of z

y9 is Element of the carrier of z

t9 is Element of the carrier of z9

u9 is Element of the carrier of z9

u is Element of the carrier of z9

u9 is Element of the carrier of z9

w9 is Element of the carrier of z9

c

c

c

c

c

the carrier of c

c

c

c

c

c

c

c

c

c

c

S is non empty non trivial OAffinSpace-like AffinStruct

(S) is non empty strict AffinStruct

the carrier of S is non empty non trivial set

the CONGR of S is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

( the carrier of S, the CONGR of S) is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

AffinStruct(# the carrier of S,( the carrier of S, the CONGR of S) #) is strict AffinStruct

the carrier of (S) is non empty set

x is Element of the carrier of (S)

z is Element of the carrier of (S)

y is Element of the carrier of (S)

t is Element of the carrier of (S)

x9 is Element of the carrier of (S)

y9 is Element of the carrier of (S)

z is Element of the carrier of (S)

x is Element of the carrier of (S)

t is Element of the carrier of (S)

y is Element of the carrier of (S)

x is Element of the carrier of (S)

y is Element of the carrier of (S)

z is Element of the carrier of (S)

t is Element of the carrier of (S)

x9 is Element of the carrier of (S)

y9 is Element of the carrier of (S)

z9 is Element of the carrier of (S)

t9 is Element of the carrier of (S)

u9 is Element of the carrier of (S)

u is Element of the carrier of (S)

u9 is Element of the carrier of (S)

w9 is Element of the carrier of (S)

c

c

x is Element of the carrier of (S)

y is Element of the carrier of (S)

z is Element of the carrier of (S)

S is non empty AffinStruct

the carrier of S is non empty set

x9 is non empty AffinStruct

the carrier of x9 is non empty set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

y9 is Element of the carrier of x9

z9 is Element of the carrier of x9

t9 is Element of the carrier of x9

u9 is Element of the carrier of x9

u is Element of the carrier of x9

u9 is Element of the carrier of x9

w9 is Element of the carrier of x9

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

S is non empty non trivial OAffinSpace-like 2-dimensional AffinStruct

the carrier of S is non empty non trivial set

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

S is non empty AffinStruct

the carrier of S is non empty set

AS is non empty non trivial OAffinSpace-like 2-dimensional AffinStruct

(AS) is non empty strict AffinStruct

the carrier of AS is non empty non trivial set

the CONGR of AS is V7() V10([: the carrier of AS, the carrier of AS:]) V11([: the carrier of AS, the carrier of AS:]) Element of bool [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:]

[: the carrier of AS, the carrier of AS:] is non empty set

[:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:] is non empty set

bool [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:] is non empty set

( the carrier of AS, the CONGR of AS) is V7() V10([: the carrier of AS, the carrier of AS:]) V11([: the carrier of AS, the carrier of AS:]) Element of bool [:[: the carrier of AS, the carrier of AS:],[: the carrier of AS, the carrier of AS:]:]

AffinStruct(# the carrier of AS,( the carrier of AS, the CONGR of AS) #) is strict AffinStruct

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of AS

y9 is Element of the carrier of AS

z9 is Element of the carrier of AS

t9 is Element of the carrier of AS

u9 is Element of the carrier of AS

u is Element of the carrier of S

the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct is non empty non trivial OAffinSpace-like 2-dimensional AffinStruct

( the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct ) is non empty strict AffinStruct

the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct is non empty non trivial set

the CONGR of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct is V7() V10([: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]) V11([: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]) Element of bool [:[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]:]

[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :] is non empty set

[:[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]:] is non empty set

bool [:[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]:] is non empty set

( the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the CONGR of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct ) is V7() V10([: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]) V11([: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]) Element of bool [:[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :],[: the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct :]:]

AffinStruct(# the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct ,( the carrier of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct , the CONGR of the non empty non trivial OAffinSpace-like 2-dimensional AffinStruct ) #) is strict AffinStruct

AS is non empty non trivial () AffinStruct

the carrier of AS is non empty non trivial set

x is Element of the carrier of AS

y is Element of the carrier of AS

z is Element of the carrier of AS

t is Element of the carrier of AS

S is non empty non trivial OAffinSpace-like 2-dimensional AffinStruct

(S) is non empty strict AffinStruct

the carrier of S is non empty non trivial set

the CONGR of S is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

[: the carrier of S, the carrier of S:] is non empty set

[:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:] is non empty set

( the carrier of S, the CONGR of S) is V7() V10([: the carrier of S, the carrier of S:]) V11([: the carrier of S, the carrier of S:]) Element of bool [:[: the carrier of S, the carrier of S:],[: the carrier of S, the carrier of S:]:]

AffinStruct(# the carrier of S,( the carrier of S, the CONGR of S) #) is strict AffinStruct

the carrier of (S) is non empty set

x is Element of the carrier of (S)

y is Element of the carrier of (S)

z is Element of the carrier of (S)

t is Element of the carrier of (S)

S is non empty AffinStruct

the carrier of S is non empty set

c

the carrier of c

AS is Element of the carrier of S

x is Element of the carrier of S

y is Element of the carrier of S

z is Element of the carrier of S

t is Element of the carrier of S

x9 is Element of the carrier of S

y9 is Element of the carrier of S

z9 is Element of the carrier of S

t9 is Element of the carrier of S

u9 is Element of the carrier of S

u is Element of the carrier of S

u9 is Element of the carrier of S

w9 is Element of the carrier of S

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c