:: MIDSP_1 semantic presentation

K122() is Element of bool K118()

K118() is set

bool K118() is non empty set

K117() is set

bool K117() is non empty set

bool K122() is non empty set

1 is non empty set

[:1,1:] is V1() non empty set

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

[:[:1,1:],1:] is V1() non empty set

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

{} is V1() V2() V3() empty set

K85({}) is non empty set

the non empty set is non empty set

[: the non empty set , the non empty set :] is V1() non empty set

[:[: the non empty set , the non empty set :], the non empty set :] is V1() non empty set

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

the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]

( the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]) is () ()

the carrier of ( the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) V6() V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]) is set

M is non empty ()

the carrier of M is non empty set

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

GS is Element of the carrier of M

x is Element of the carrier of M

the of M . (GS,x) is Element of the carrier of M

op2 is V1() V4([:1,1:]) V5(1) V6() V18([:1,1:],1) Element of bool [:[:1,1:],1:]

(1,op2) is () ()

() is ()

the carrier of () is non empty set

[: the carrier of (), the carrier of ():] is V1() non empty set

the of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) V6() V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]

[:[: the carrier of (), the carrier of ():], the carrier of ():] is V1() non empty set

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

M is Element of the carrier of ()

GS is Element of the carrier of ()

((),M,GS) is Element of the carrier of ()

the of () . (M,GS) is Element of the carrier of ()

op2 . (M,GS) is set

M is Element of the carrier of ()

((),M,M) is Element of the carrier of ()

the of () . (M,M) is Element of the carrier of ()

GS is Element of the carrier of ()

((),M,GS) is Element of the carrier of ()

the of () . (M,GS) is Element of the carrier of ()

((),GS,M) is Element of the carrier of ()

the of () . (GS,M) is Element of the carrier of ()

x is Element of the carrier of ()

y is Element of the carrier of ()

((),x,y) is Element of the carrier of ()

the of () . (x,y) is Element of the carrier of ()

((),((),M,GS),((),x,y)) is Element of the carrier of ()

the of () . (((),M,GS),((),x,y)) is Element of the carrier of ()

((),M,x) is Element of the carrier of ()

the of () . (M,x) is Element of the carrier of ()

((),GS,y) is Element of the carrier of ()

the of () . (GS,y) is Element of the carrier of ()

((),((),M,x),((),GS,y)) is Element of the carrier of ()

the of () . (((),M,x),((),GS,y)) is Element of the carrier of ()

xx is Element of the carrier of ()

((),xx,M) is Element of the carrier of ()

the of () . (xx,M) is Element of the carrier of ()

M is non empty () ()

the carrier of M is non empty set

y is Element of the carrier of M

xx is Element of the carrier of M

(M,y,xx) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (y,xx) is Element of the carrier of M

(M,xx,y) is Element of the carrier of M

the of M . (xx,y) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

y is Element of the carrier of M

(M,(M,GS,x),y) is Element of the carrier of M

the of M . ((M,GS,x),y) is Element of the carrier of M

(M,GS,y) is Element of the carrier of M

the of M . (GS,y) is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M . (x,y) is Element of the carrier of M

(M,(M,GS,y),(M,x,y)) is Element of the carrier of M

the of M . ((M,GS,y),(M,x,y)) is Element of the carrier of M

(M,y,y) is Element of the carrier of M

the of M . (y,y) is Element of the carrier of M

(M,(M,GS,x),(M,y,y)) is Element of the carrier of M

the of M . ((M,GS,x),(M,y,y)) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

y is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M . (x,y) is Element of the carrier of M

(M,GS,(M,x,y)) is Element of the carrier of M

the of M . (GS,(M,x,y)) is Element of the carrier of M

(M,GS,y) is Element of the carrier of M

the of M . (GS,y) is Element of the carrier of M

(M,(M,GS,x),(M,GS,y)) is Element of the carrier of M

the of M . ((M,GS,x),(M,GS,y)) is Element of the carrier of M

(M,GS,GS) is Element of the carrier of M

the of M . (GS,GS) is Element of the carrier of M

(M,(M,GS,GS),(M,x,y)) is Element of the carrier of M

the of M . ((M,GS,GS),(M,x,y)) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

y is Element of the carrier of M

(M,y,GS) is Element of the carrier of M

the of M . (y,GS) is Element of the carrier of M

(M,(M,y,GS),x) is Element of the carrier of M

the of M . ((M,y,GS),x) is Element of the carrier of M

(M,y,x) is Element of the carrier of M

the of M . (y,x) is Element of the carrier of M

(M,(M,y,x),GS) is Element of the carrier of M

the of M . ((M,y,x),GS) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

y is Element of the carrier of M

(M,y,x) is Element of the carrier of M

the of M . (y,x) is Element of the carrier of M

xx is Element of the carrier of M

(M,xx,x) is Element of the carrier of M

the of M . (xx,x) is Element of the carrier of M

(M,GS,(M,xx,x)) is Element of the carrier of M

the of M . (GS,(M,xx,x)) is Element of the carrier of M

(M,GS,xx) is Element of the carrier of M

the of M . (GS,xx) is Element of the carrier of M

(M,(M,GS,xx),(M,y,x)) is Element of the carrier of M

the of M . ((M,GS,xx),(M,y,x)) is Element of the carrier of M

(M,GS,y) is Element of the carrier of M

the of M . (GS,y) is Element of the carrier of M

(M,GS,(M,GS,y)) is Element of the carrier of M

the of M . (GS,(M,GS,y)) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

y is Element of the carrier of M

(M,GS,y) is Element of the carrier of M

the of M . (GS,y) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

y is Element of the carrier of M

xx is Element of the carrier of M

(M,GS,xx) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,xx) is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M . (x,y) is Element of the carrier of M

(M,y,x) is Element of the carrier of M

the of M . (y,x) is Element of the carrier of M

(M,xx,GS) is Element of the carrier of M

the of M . (xx,GS) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

y is Element of the carrier of M

(M,GS,y) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,y) is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M . (GS,x) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

y is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

(M,x,GS) is Element of the carrier of M

the of M . (x,GS) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

y is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (x,y) is Element of the carrier of M

xx is Element of the carrier of M

(M,xx,GS) is Element of the carrier of M

the of M . (xx,GS) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

y is Element of the carrier of M

xx is Element of the carrier of M

yy is Element of the carrier of M

(M,GS,xx) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,xx) is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M . (x,y) is Element of the carrier of M

(M,GS,yy) is Element of the carrier of M

the of M . (GS,yy) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

y is Element of the carrier of M

xx is Element of the carrier of M

yy is Element of the carrier of M

yy is Element of the carrier of M

(M,x,GS) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (x,GS) is Element of the carrier of M

(M,y,yy) is Element of the carrier of M

the of M . (y,yy) is Element of the carrier of M

(M,(M,x,GS),(M,y,yy)) is Element of the carrier of M

the of M . ((M,x,GS),(M,y,yy)) is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M . (x,y) is Element of the carrier of M

(M,GS,yy) is Element of the carrier of M

the of M . (GS,yy) is Element of the carrier of M

(M,(M,x,y),(M,GS,yy)) is Element of the carrier of M

the of M . ((M,x,y),(M,GS,yy)) is Element of the carrier of M

(M,GS,xx) is Element of the carrier of M

the of M . (GS,xx) is Element of the carrier of M

(M,(M,GS,xx),(M,GS,yy)) is Element of the carrier of M

the of M . ((M,GS,xx),(M,GS,yy)) is Element of the carrier of M

(M,x,yy) is Element of the carrier of M

the of M . (x,yy) is Element of the carrier of M

(M,(M,GS,xx),(M,x,yy)) is Element of the carrier of M

the of M . ((M,GS,xx),(M,x,yy)) is Element of the carrier of M

(M,xx,yy) is Element of the carrier of M

the of M . (xx,yy) is Element of the carrier of M

(M,(M,x,GS),(M,xx,yy)) is Element of the carrier of M

the of M . ((M,x,GS),(M,xx,yy)) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

y is Element of the carrier of M

xx is Element of the carrier of M

yy is Element of the carrier of M

yy is Element of the carrier of M

(M,xx,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (xx,x) is Element of the carrier of M

(M,GS,yy) is Element of the carrier of M

the of M . (GS,yy) is Element of the carrier of M

(M,(M,xx,x),(M,GS,yy)) is Element of the carrier of M

the of M . ((M,xx,x),(M,GS,yy)) is Element of the carrier of M

(M,GS,xx) is Element of the carrier of M

the of M . (GS,xx) is Element of the carrier of M

(M,x,yy) is Element of the carrier of M

the of M . (x,yy) is Element of the carrier of M

(M,(M,GS,xx),(M,x,yy)) is Element of the carrier of M

the of M . ((M,GS,xx),(M,x,yy)) is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M . (x,y) is Element of the carrier of M

(M,(M,x,y),(M,x,yy)) is Element of the carrier of M

the of M . ((M,x,y),(M,x,yy)) is Element of the carrier of M

(M,yy,xx) is Element of the carrier of M

the of M . (yy,xx) is Element of the carrier of M

(M,(M,yy,xx),(M,x,y)) is Element of the carrier of M

the of M . ((M,yy,xx),(M,x,y)) is Element of the carrier of M

(M,yy,y) is Element of the carrier of M

the of M . (yy,y) is Element of the carrier of M

(M,(M,xx,x),(M,yy,y)) is Element of the carrier of M

the of M . ((M,xx,x),(M,yy,y)) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

y is Element of [: the carrier of M, the carrier of M:]

y `1 is Element of the carrier of M

y `2 is Element of the carrier of M

y is Element of [: the carrier of M, the carrier of M:]

y `1 is Element of the carrier of M

y `2 is Element of the carrier of M

xx is Element of [: the carrier of M, the carrier of M:]

xx `1 is Element of the carrier of M

xx `2 is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

y is Element of the carrier of M

xx is Element of the carrier of M

[y,xx] is Element of [: the carrier of M, the carrier of M:]

[GS,x] `1 is Element of the carrier of M

[GS,x] `2 is Element of the carrier of M

[y,xx] `1 is Element of the carrier of M

[y,xx] `2 is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

y is Element of the carrier of M

xx is Element of the carrier of M

[y,xx] is Element of [: the carrier of M, the carrier of M:]

[GS,x] `1 is Element of the carrier of M

[GS,x] `2 is Element of the carrier of M

[y,xx] `1 is Element of the carrier of M

[y,xx] `2 is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

x is Element of [: the carrier of M, the carrier of M:]

y is Element of [: the carrier of M, the carrier of M:]

GS `1 is Element of the carrier of M

GS `2 is Element of the carrier of M

x `1 is Element of the carrier of M

x `2 is Element of the carrier of M

y `1 is Element of the carrier of M

y `2 is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

x is Element of [: the carrier of M, the carrier of M:]

y is Element of [: the carrier of M, the carrier of M:]

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

x is Element of [: the carrier of M, the carrier of M:]

y is Element of [: the carrier of M, the carrier of M:]

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

x is Element of [: the carrier of M, the carrier of M:]

y is Element of [: the carrier of M, the carrier of M:]

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

GS is Element of [: the carrier of M, the carrier of M:]

{ b

y is set

xx is Element of [: the carrier of M, the carrier of M:]

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

{ b

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

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

(M,GS) is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:]

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

{ b

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

x is Element of [: the carrier of M, the carrier of M:]

(M,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

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

{ b

y is Element of [: the carrier of M, the carrier of M:]

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

(M,GS) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

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

{ b

x is Element of [: the carrier of M, the carrier of M:]

(M,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

{ b

y is set

xx is Element of [: the carrier of M, the carrier of M:]

xx is Element of [: the carrier of M, the carrier of M:]

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

(M,GS) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

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

{ b

x is Element of [: the carrier of M, the carrier of M:]

(M,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[GS,x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

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

{ b

y is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (x,y) is Element of the carrier of M

xx is Element of the carrier of M

[y,xx] is Element of [: the carrier of M, the carrier of M:]

(M,[y,xx]) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

{ b

(M,GS,xx) is Element of the carrier of M

the of M . (GS,xx) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

(M,GS) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

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

{ b

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

the Element of [: the carrier of M, the carrier of M:] is Element of [: the carrier of M, the carrier of M:]

(M, the Element of [: the carrier of M, the carrier of M:]) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

{ b

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is Element of [: the carrier of M, the carrier of M:]

(M,GS) is V1() V4( the carrier of M) V5( the carrier of M) non empty Element of bool [: the carrier of M, the carrier of M:]

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

{ b

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

the Element of the carrier of M is Element of the carrier of M

[ the Element of the carrier of M, the Element of the carrier of M] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M, the Element of the carrier of M]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

x is Element of [: the carrier of M, the carrier of M:]

x `1 is Element of the carrier of M

x `2 is Element of the carrier of M

[ the Element of the carrier of M, the Element of the carrier of M] `1 is Element of the carrier of M

[ the Element of the carrier of M, the Element of the carrier of M] `2 is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

x is set

y is Element of [: the carrier of M, the carrier of M:]

y `1 is Element of the carrier of M

y `2 is Element of the carrier of M

y is Element of [: the carrier of M, the carrier of M:]

y `1 is Element of the carrier of M

y `2 is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

GS is Element of the carrier of M

[GS,GS] is Element of [: the carrier of M, the carrier of M:]

(M,[GS,GS]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

x is Element of [: the carrier of M, the carrier of M:]

x `1 is Element of the carrier of M

x `2 is Element of the carrier of M

y is Element of [: the carrier of M, the carrier of M:]

y `1 is Element of the carrier of M

y `2 is Element of the carrier of M

[GS,GS] `1 is Element of the carrier of M

[GS,GS] `2 is Element of the carrier of M

[GS,GS] `1 is Element of the carrier of M

[GS,GS] `2 is Element of the carrier of M

x `1 is Element of the carrier of M

x `2 is Element of the carrier of M

x is set

y is set

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

yy is Element of [: the carrier of M, the carrier of M:]

(M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy is Element of [: the carrier of M, the carrier of M:]

(M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy `2 is Element of the carrier of M

yy `1 is Element of the carrier of M

yy `1 is Element of the carrier of M

yy `2 is Element of the carrier of M

[(yy `1),(yy `2)] is Element of [: the carrier of M, the carrier of M:]

(M,[(yy `1),(yy `2)]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

zz is Element of [: the carrier of M, the carrier of M:]

(M,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

q9 is Element of [: the carrier of M, the carrier of M:]

(M,q9) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

zz `2 is Element of the carrier of M

q9 `1 is Element of the carrier of M

zz `1 is Element of the carrier of M

q9 `2 is Element of the carrier of M

[(zz `1),(q9 `2)] is Element of [: the carrier of M, the carrier of M:]

(M,[(zz `1),(q9 `2)]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

y is Element of [: the carrier of M, the carrier of M:]

(M,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

xx is Element of [: the carrier of M, the carrier of M:]

(M,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

xx `1 is Element of the carrier of M

xx `2 is Element of the carrier of M

y `2 is Element of the carrier of M

yy is Element of the carrier of M

y `1 is Element of the carrier of M

[(y `1),yy] is Element of [: the carrier of M, the carrier of M:]

(M,[(y `1),yy]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy is Element of [: the carrier of M, the carrier of M:]

(M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy `2 is Element of the carrier of M

yy `1 is Element of the carrier of M

[(y `2),yy] is Element of [: the carrier of M, the carrier of M:]

zz is Element of [: the carrier of M, the carrier of M:]

(M,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

zz `1 is Element of the carrier of M

zz `2 is Element of the carrier of M

[(yy `1),(zz `2)] is Element of [: the carrier of M, the carrier of M:]

(M,[(yy `1),(zz `2)]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy is Element of [: the carrier of M, the carrier of M:]

(M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy is Element of [: the carrier of M, the carrier of M:]

(M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy `2 is Element of the carrier of M

yy `1 is Element of the carrier of M

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

yy `1 is Element of the carrier of M

yy `2 is Element of the carrier of M

[(yy `1),(yy `2)] is Element of [: the carrier of M, the carrier of M:]

(M,[(yy `1),(yy `2)]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

zz is Element of [: the carrier of M, the carrier of M:]

(M,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

q9 is Element of [: the carrier of M, the carrier of M:]

(M,q9) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

zz `2 is Element of the carrier of M

q9 `1 is Element of the carrier of M

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

zz `1 is Element of the carrier of M

q9 `2 is Element of the carrier of M

[(zz `1),(q9 `2)] is Element of [: the carrier of M, the carrier of M:]

(M,[(zz `1),(q9 `2)]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[: the carrier of M, the carrier of M:] is V1() non empty set

y is Element of [: the carrier of M, the carrier of M:]

(M,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

y `1 is Element of the carrier of M

y `2 is Element of the carrier of M

xx is Element of the carrier of M

[(y `1),(y `2)] is Element of [: the carrier of M, the carrier of M:]

[GS,xx] is Element of [: the carrier of M, the carrier of M:]

(M,[GS,xx]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[GS,x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

y is Element of the carrier of M

[GS,y] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[GS,y]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,GS,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

y is Element of the carrier of M

xx is Element of the carrier of M

[y,xx] is Element of [: the carrier of M, the carrier of M:]

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,[GS,x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,y,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,[y,xx]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[GS,x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

y is Element of the carrier of M

xx is Element of the carrier of M

(M,y,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[y,xx] is Element of [: the carrier of M, the carrier of M:]

(M,[y,xx]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,GS,xx) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,xx) is Element of the carrier of M

(M,x,y) is Element of the carrier of M

the of M . (x,y) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

GS is Element of the carrier of M

(M,GS,GS) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,GS] is Element of [: the carrier of M, the carrier of M:]

(M,[GS,GS]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[GS,x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

y is Element of the carrier of M

(M,GS,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,y] is Element of [: the carrier of M, the carrier of M:]

(M,[GS,y]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,x] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[GS,x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

y is Element of the carrier of M

(M,x,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

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

(M,[x,y]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,(M,GS,x),(M,x,y)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,y] is Element of [: the carrier of M, the carrier of M:]

(M,[GS,y]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

[GS,x] `2 is Element of the carrier of M

[x,y] `1 is Element of the carrier of M

[x,y] `2 is Element of the carrier of M

(M,(M,[GS,x]),(M,[x,y])) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,x] `1 is Element of the carrier of M

[([GS,x] `1),([x,y] `2)] is Element of [: the carrier of M, the carrier of M:]

(M,[([GS,x] `1),([x,y] `2)]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

[GS,(M,GS,x)] is Element of [: the carrier of M, the carrier of M:]

[(M,GS,x),x] is Element of [: the carrier of M, the carrier of M:]

(M,(M,GS,x),(M,GS,x)) is Element of the carrier of M

the of M . ((M,GS,x),(M,GS,x)) is Element of the carrier of M

M is non empty () ()

the carrier of M is non empty set

GS is Element of the carrier of M

x is Element of the carrier of M

(M,GS,x) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . (GS,x) is Element of the carrier of M

(M,GS,(M,GS,x)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,(M,GS,x)] is Element of [: the carrier of M, the carrier of M:]

(M,[GS,(M,GS,x)]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,(M,GS,(M,GS,x)),(M,GS,(M,GS,x))) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[GS,x] is Element of [: the carrier of M, the carrier of M:]

(M,[GS,x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,(M,GS,x),x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[(M,GS,x),x] is Element of [: the carrier of M, the carrier of M:]

(M,[(M,GS,x),x]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,(M,GS,(M,GS,x)),(M,(M,GS,x),x)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

the carrier of M is non empty set

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,(M,GS,x),y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,x,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,(M,x,y)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

the Element of the carrier of M is Element of the carrier of M

yy is Element of the carrier of M

(M, the Element of the carrier of M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,yy] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[ the Element of the carrier of M,yy]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy is Element of the carrier of M

(M,yy,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[yy,yy] is Element of [: the carrier of M, the carrier of M:]

(M,[yy,yy]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

zz is Element of the carrier of M

(M,yy,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[yy,zz] is Element of [: the carrier of M, the carrier of M:]

(M,[yy,zz]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M, the Element of the carrier of M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,yy] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M,yy]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,(M, the Element of the carrier of M,yy),y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M, the Element of the carrier of M,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,zz] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M,zz]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,yy,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[yy,zz] is Element of [: the carrier of M, the carrier of M:]

(M,[yy,zz]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,(M, the Element of the carrier of M,yy),(M,yy,zz)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

the carrier of M is non empty set

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,(M)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

the Element of the carrier of M is Element of the carrier of M

y is Element of the carrier of M

(M, the Element of the carrier of M,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,y] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M,y]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,y,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[y,y] is Element of [: the carrier of M, the carrier of M:]

(M,[y,y]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,(M, the Element of the carrier of M,y),(M,y,y)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

the carrier of M is non empty set

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

the Element of the carrier of M is Element of the carrier of M

y is Element of the carrier of M

(M, the Element of the carrier of M,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,y] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M,y]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,y, the Element of the carrier of M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[y, the Element of the carrier of M] is Element of [: the carrier of M, the carrier of M:]

(M,[y, the Element of the carrier of M]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M,GS,(M,y, the Element of the carrier of M)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M, the Element of the carrier of M, the Element of the carrier of M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M, the Element of the carrier of M] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M, the Element of the carrier of M]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,x,GS) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

the Element of the carrier of M is Element of the carrier of M

xx is Element of the carrier of M

(M, the Element of the carrier of M,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,xx] is Element of [: the carrier of M, the carrier of M:]

[: the carrier of M, the carrier of M:] is V1() non empty set

(M,[ the Element of the carrier of M,xx]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy is Element of the carrier of M

(M,xx,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[xx,yy] is Element of [: the carrier of M, the carrier of M:]

(M,[xx,yy]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

yy is Element of the carrier of M

(M, the Element of the carrier of M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,yy] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M,yy]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

zz is Element of the carrier of M

(M,yy,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[yy,zz] is Element of [: the carrier of M, the carrier of M:]

(M,[yy,zz]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M, the Element of the carrier of M,zz) is Element of the carrier of M

the of M is V1() V4([: the carrier of M, the carrier of M:]) V5( the carrier of M) V6() V18([: the carrier of M, the carrier of M:], the carrier of M) Element of bool [:[: the carrier of M, the carrier of M:], the carrier of M:]

[:[: the carrier of M, the carrier of M:], the carrier of M:] is V1() non empty set

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

the of M . ( the Element of the carrier of M,zz) is Element of the carrier of M

(M,xx,yy) is Element of the carrier of M

the of M . (xx,yy) is Element of the carrier of M

(M, the Element of the carrier of M,yy) is Element of the carrier of M

the of M . ( the Element of the carrier of M,yy) is Element of the carrier of M

(M, the Element of the carrier of M,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,yy] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M,yy]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

(M, the Element of the carrier of M,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[ the Element of the carrier of M,zz] is Element of [: the carrier of M, the carrier of M:]

(M,[ the Element of the carrier of M,zz]) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

the carrier of M is non empty set

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,x,(M)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,(M,GS,xx),x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,xx,GS) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,(M,xx,GS),x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,xx,(M,GS,y)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,(M,xx,GS),y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,(M),y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,y,(M)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

the carrier of M is non empty set

GS is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,x) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,GS,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

M is non empty () ()

the carrier of M is non empty set

(M) is set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

GS is set

x is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:]

M is non empty () ()

(M) is set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

GS is Element of (M)

x is Element of (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,y,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

yy is Element of (M)

yy is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

zz is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,yy,zz) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

yy is Element of (M)

yy is Element of (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,y,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

GS is Element of (M)

x is Element of (M)

(M,GS,x) is Element of (M)

(M,x,GS) is Element of (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,y,xx) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,xx,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

GS is Element of (M)

x is Element of (M)

(M,GS,x) is Element of (M)

y is Element of (M)

(M,(M,GS,x),y) is Element of (M)

(M,x,y) is Element of (M)

(M,GS,(M,x,y)) is Element of (M)

yy is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

yy is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,yy,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,xx,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,(M,xx,yy),yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,xx,(M,yy,yy)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

[:(M),(M):] is V1() non empty set

[:[:(M),(M):],(M):] is V1() non empty set

bool [:[:(M),(M):],(M):] is non empty set

GS is Element of (M)

x is Element of (M)

(M,GS,x) is Element of (M)

GS is V1() V4([:(M),(M):]) V5((M)) V6() V18([:(M),(M):],(M)) Element of bool [:[:(M),(M):],(M):]

x is Element of (M)

y is Element of (M)

GS . (x,y) is Element of (M)

(M,x,y) is Element of (M)

GS is V1() V4([:(M),(M):]) V5((M)) V6() V18([:(M),(M):],(M)) Element of bool [:[:(M),(M):],(M):]

x is V1() V4([:(M),(M):]) V5((M)) V6() V18([:(M),(M):],(M)) Element of bool [:[:(M),(M):],(M):]

y is Element of (M)

xx is Element of (M)

GS . (y,xx) is Element of (M)

x . (y,xx) is Element of (M)

(M,y,xx) is Element of (M)

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

GS is Element of (M)

x is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

y is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,x,y) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

xx is Element of (M)

(M,GS,xx) is Element of (M)

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

GS is Element of (M)

x is Element of (M)

(M,GS,x) is Element of (M)

y is Element of (M)

(M,GS,y) is Element of (M)

xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

yy is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,xx,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

yy is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

(M,xx,yy) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

[:(M),(M):] is V1() non empty set

bool [:(M),(M):] is non empty set

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

GS is Element of (M)

GS is V1() V4((M)) V5((M)) V6() V18((M),(M)) Element of bool [:(M),(M):]

x is Element of (M)

GS . x is Element of (M)

(M,x,(GS . x)) is Element of (M)

GS is V1() V4((M)) V5((M)) V6() V18((M),(M)) Element of bool [:(M),(M):]

x is V1() V4((M)) V5((M)) V6() V18((M),(M)) Element of bool [:(M),(M):]

y is Element of (M)

GS . y is Element of (M)

x . y is Element of (M)

(M,y,(GS . y)) is Element of (M)

(M,y,(x . y)) is Element of (M)

M is non empty () ()

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

{ b

(M) is non empty set

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

{ b

M is non empty () ()

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

(M) is V1() V4([:(M),(M):]) V5((M)) V6() V18([:(M),(M):],(M)) Element of bool [:[:(M),(M):],(M):]

[:(M),(M):] is V1() non empty set

[:[:(M),(M):],(M):] is V1() non empty set

bool [:[:(M),(M):],(M):] is non empty set

(M) is Element of (M)

(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)

{ b

addLoopStr(# (M),(M),(M) #) is strict addLoopStr

M is non empty () ()

(M) is addLoopStr

(M) is non empty set

the carrier of M is non empty set

[: the carrier of M, the carrier of M:] is V1() non empty set

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

{ b

(M) is V1() V4([:(