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:]
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,GS) } is set
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:]
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,GS) } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,GS) } 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 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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,x) } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,GS) } is set
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:]
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,x) } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,GS) } is set
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:]
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,x) } is 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
[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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,x]) } is set
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:]
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[y,xx]) } is set
(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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,GS) } 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
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:]
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1, the Element of [: the carrier of M, the carrier of M:]) } 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 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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,GS) } 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
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M, the Element of the carrier of M]) } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,GS]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,yy) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,yy) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[(yy `1),(yy `2)]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,zz) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,q9) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[(zz `1),(q9 `2)]) } 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 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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,y) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,xx) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[(y `1),yy]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,yy) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,zz) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[(yy `1),(zz `2)]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,yy) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,yy) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[(yy `1),(yy `2)]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,zz) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,q9) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[(zz `1),(q9 `2)]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,y) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,xx]) } is 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
[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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,x]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,y]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,x]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[y,xx]) } is 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 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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,x]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[y,xx]) } is set
(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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,GS]) } is 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 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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,x]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,y]) } is 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 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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,x]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[x,y]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,y]) } is set
[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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[([GS,x] `1),([x,y] `2)]) } is 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
[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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,(M,GS,x)]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[GS,x]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[(M,GS,x),x]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,yy]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[yy,yy]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[yy,zz]) } is 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)
[ 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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,yy]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,zz]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[yy,zz]) } is set
(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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,y]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[y,y]) } is set
(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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,y]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[y, the Element of the carrier of M]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M, the Element of the carrier of M]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,xx]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[xx,yy]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,yy]) } is set
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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[yy,zz]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,yy]) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : (M,b1,[ the Element of the carrier of M,zz]) } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
[:(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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(M) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
[:(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
(M) is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
addLoopStr(# (M),(M),(M) #) is strict addLoopStr
M is non empty () ()
(M) is non empty strict 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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
addLoopStr(# (M),(M),(M) #) is strict addLoopStr
the carrier of (M) is non empty set
M is non empty () ()
(M) is non empty strict 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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
addLoopStr(# (M),(M),(M) #) is strict addLoopStr
the carrier of (M) is non empty set
[: the carrier of (M), the carrier of (M):] is V1() non empty set
the addF 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
M is non empty () ()
(M) is non empty strict 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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
addLoopStr(# (M),(M),(M) #) is strict addLoopStr
0. (M) is V51((M)) Element of the carrier of (M)
the carrier of (M) is non empty set
the ZeroF of (M) is Element of the carrier of (M)
M is non empty () ()
(M) is non empty strict 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
{ b1 where b1 is V1() V4( the carrier of M) V5( the carrier of M) Element of bool [: the carrier of M, the carrier of M:] : b1 is V1() V4( the carrier of M) V5( the carrier of M) non empty (M) } is set
(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)
{ b1 where b1 is Element of [: the carrier of M, the carrier of M:] : b1 `1 = b1 `2 } is set
addLoopStr(# (M),(M),(M) #) is strict addLoopStr
the carrier of (M) is non empty set
x is Element of the carrier of (M)
y is Element of the carrier of (M)
x + y is Element of the carrier of (M)
the addF 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 addF of (M) . (x,y) is Element of the carrier of (M)
xx is Element of the carrier of (M)
(x + y) + xx is Element of the carrier of (M)
the addF of (M) . ((x + y),xx) is Element of the carrier of (M)
y + xx is Element of the carrier of (M)
the addF of (M) . (y,xx) is Element of the carrier of (M)
x + (y + xx) is Element of the carrier of (M)
the addF of (M) . (x,(y + xx)) is Element of the carrier of (M)
yy is Element of (M)
yy is Element of (M)
(M,yy,yy) is Element of (M)
zz is Element of (M)
(M) . ((M,yy,yy),zz) is Element of (M)
(M,(M,yy,yy),zz) is Element of (M)
(M,yy,zz) is Element of (M)
(M,yy,(M,yy,zz)) is Element of (M)
(M) . (yy,(M,yy,zz)) is Element of (M)
the carrier of (M) is non empty set
x is Element of the carrier of (M)
0. (M) is V51((M)) Element of the carrier of (M)
the ZeroF of (M) is Element of the carrier of (M)
x + (0. (M)) is Element of the carrier of (M)
the addF 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 addF of (M) . (x,(0. (M))) is Element of the carrier of (M)
y is Element of (M)
(M,y,(M)) is Element of (M)
xx is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)
(M,xx,(M)) is V1() V4( the carrier of M) V5( the carrier of M) non empty (M)
the carrier of (M) is non empty set
x is Element of the carrier of (M)
(M) is V1() V4((M)) V5((M)) V6() V18((M),(M)) Element of bool [:(M),(M):]
bool [:(M),(M):] is non empty set
y is Element of (M)
(M) . y is Element of (M)
xx is Element of the carrier of (M)
x + xx is Element of the carrier of (M)
the addF 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 addF of (M) . (x,xx) is Element of the carrier of (M)
0. (M) is V51((M)) Element of the carrier of (M)
the ZeroF of (M) is Element of the carrier of (M)
(M,y,((M) . y)) is Element of (M)
the carrier of (M) is non empty set
x is Element of the carrier of (M)
y is Element of the carrier of (M)
x + y is Element of the carrier of (M)
the addF 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 addF of (M) . (x,y) is Element of the carrier of (M)
y + x is Element of the carrier of (M)
the addF of (M) . (y,x) is Element of the carrier of (M)
xx is Element of (M)
yy is Element of (M)
(M,xx,yy) is Element of (M)
(M,yy,xx) is Element of (M)