:: FINTOPO2 semantic presentation

K135() is Element of bool K131()
K131() is set
bool K131() is non empty set
K130() is set
bool K130() is non empty set
bool K135() is non empty set
BOOLEAN is set
{} is empty set
the empty set is empty set
1 is non empty set
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A ^i is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : U_FT b₁ c= A } is set
B ^i is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : U_FT b₁ c= B } is set
C is set
y is Element of the carrier of FMT
U_FT y is Element of bool the carrier of FMT
z is Element of the carrier of FMT
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ^delta is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : ( not U_FT b<sub>1</sub> misses A & not U_FT b<sub>1</sub> misses A ` ) } is set
A ^b is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : not U_FT b₁ misses A } is set
A ^i is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : U_FT b₁ c= A } is set
(A ^i) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A ^i) is set
(A ^b) /\ ((A ^i) `) is Element of bool the carrier of FMT
B is set
C is Element of the carrier of FMT
U_FT C is Element of bool the carrier of FMT
(A `) ^b is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : not U_FT b<sub>1</sub> misses A ` } is set
((A `) ^b) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((A `) ^b) is set
(((A `) ^b) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (((A `) ^b) `) is set
(A `) ^b is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : not U_FT b<sub>1</sub> misses A ` } is set
((A `) ^b) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((A `) ^b) is set
(((A `) ^b) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (((A `) ^b) `) is set
C is Element of the carrier of FMT
U_FT C is Element of bool the carrier of FMT
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ^delta is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : ( not U_FT b<sub>1</sub> misses A & not U_FT b<sub>1</sub> misses A ` ) } is set
A ^b is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : not U_FT b₁ misses A } is set
A ^i is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : U_FT b₁ c= A } is set
(A ^b) \ (A ^i) is Element of bool the carrier of FMT
B is set
(A ^i) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A ^i) is set
(A ^b) /\ ((A ^i) `) is Element of bool the carrier of FMT
(A ^i) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A ^i) is set
(A ^b) /\ ((A ^i) `) is Element of bool the carrier of FMT
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
(A `) ^i is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : U_FT b₁ c= A ` } is set
(A `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A `) is set
((A `) `) ^b is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : not U_FT b₁ misses (A `) ` } is set
(((A `) `) ^b) ` is Element of bool the carrier of FMT
the carrier of FMT \ (((A `) `) ^b) is set
A ^b is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : not U_FT b<sub>1</sub> misses A } is set
(A ^b) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A ^b) is set
((A ^b) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((A ^b) `) is set
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
(A `) ^b is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : not U_FT b<sub>1</sub> misses A ` } is set
(A `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A `) is set
((A `) `) ^i is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : U_FT b<sub>1</sub> c= (A `) ` } is set
(((A `) `) ^i) ` is Element of bool the carrier of FMT
the carrier of FMT \ (((A `) `) ^i) is set
A ^i is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : U_FT b₁ c= A } is set
(A ^i) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A ^i) is set
((A ^i) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((A ^i) `) is set
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
B is Element of the carrier of FMT
A is Element of the carrier of FMT
U_FT A is Element of bool the carrier of FMT
C is Element of bool the carrier of FMT
TRUE is Element of BOOLEAN
FALSE is Element of BOOLEAN
K136() is empty Element of K135()
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
B is Element of the carrier of FMT
A is Element of the carrier of FMT
U_FT A is Element of bool the carrier of FMT
C is Element of bool the carrier of FMT
C ` is Element of bool the carrier of FMT
the carrier of FMT \ C is set
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
y is non empty RelStr
the carrier of y is non empty set
bool the carrier of y is non empty set
A is Element of the carrier of FMT
B is Element of the carrier of FMT
C is Element of bool the carrier of FMT
(FMT,A,B,C) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
W is Element of the carrier of y
z is Element of the carrier of y
U_FT z is Element of bool the carrier of y
c<sub>8</sub> is Element of bool the carrier of y
(y,z,W,c<sub>8</sub>) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
y is non empty RelStr
the carrier of y is non empty set
bool the carrier of y is non empty set
A is Element of the carrier of FMT
B is Element of the carrier of FMT
C is Element of bool the carrier of FMT
(FMT,A,B,C) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
C ` is Element of bool the carrier of FMT
the carrier of FMT \ C is set
W is Element of the carrier of y
z is Element of the carrier of y
U_FT z is Element of bool the carrier of y
c₈ is Element of bool the carrier of y
c₈ ` is Element of bool the carrier of y
the carrier of y \ c<sub>8</sub> is set
(y,z,W,c<sub>8</sub>) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^delta is Element of bool the carrier of FMT
B ` is Element of bool the carrier of FMT
the carrier of FMT \ B is set
{ b₁ where b₁ is Element of the carrier of FMT : ( not U_FT b₁ misses B & not U_FT b₁ misses B ` ) } is set
C is Element of the carrier of FMT
U_FT C is Element of bool the carrier of FMT
y is set
z is Element of the carrier of FMT
(FMT,A,z,B) is Element of BOOLEAN
W is set
(FMT,A,W,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
(U_FT A) /\ B is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
z is Element of the carrier of FMT
(FMT,A,z,B) is Element of BOOLEAN
W is Element of the carrier of FMT
(FMT,A,W,B) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
B is Element of the carrier of FMT
A is Element of the carrier of FMT
U_FT A is Element of bool the carrier of FMT
bool the carrier of FMT is non empty set
FMT is non empty RelStr
the carrier of FMT is non empty set
C is non empty RelStr
the carrier of C is non empty set
A is Element of the carrier of FMT
B is Element of the carrier of FMT
(FMT,A,B) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
bool the carrier of FMT is non empty set
z is Element of the carrier of C
y is Element of the carrier of C
U_FT y is Element of bool the carrier of C
bool the carrier of C is non empty set
(C,y,z) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^i is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : U_FT b<sub>1</sub> c= B } is set
U_FT A is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C) is Element of BOOLEAN
(FMT,A,C,B) is Element of BOOLEAN
C is Element of the carrier of FMT
U_FT A is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C) is Element of BOOLEAN
(FMT,A,C,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C) is Element of BOOLEAN
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y) is Element of BOOLEAN
(FMT,A,y,B) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^b is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : not U_FT b<sub>1</sub> misses B } is set
C is Element of the carrier of FMT
U_FT C is Element of bool the carrier of FMT
y is set
z is Element of the carrier of FMT
(FMT,A,z,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
(U_FT A) /\ B is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
C is non empty RelStr
the carrier of C is non empty set
bool the carrier of C is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
(FMT,A,B) is Element of BOOLEAN
y is Element of the carrier of C
z is Element of bool the carrier of C
(C,y,z) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^deltai is Element of bool the carrier of FMT
B ^delta is Element of bool the carrier of FMT
B ` is Element of bool the carrier of FMT
the carrier of FMT \ B is set
{ b₁ where b₁ is Element of the carrier of FMT : ( not U_FT b₁ misses B & not U_FT b₁ misses B ` ) } is set
B /\ (B ^delta) is Element of bool the carrier of FMT
(FMT,A,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
z is Element of the carrier of FMT
(FMT,A,z,B) is Element of BOOLEAN
W is Element of the carrier of FMT
(FMT,A,W,B) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^deltao is Element of bool the carrier of FMT
B ` is Element of bool the carrier of FMT
the carrier of FMT \ B is set
B ^delta is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( not U_FT b₁ misses B & not U_FT b₁ misses B ` ) } is set
(B `) /\ (B ^delta) is Element of bool the carrier of FMT
(FMT,A,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
z is Element of the carrier of FMT
(FMT,A,z,B) is Element of BOOLEAN
W is Element of the carrier of FMT
(FMT,A,W,B) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of the carrier of FMT
FMT is non empty RelStr
the carrier of FMT is non empty set
C is non empty RelStr
the carrier of C is non empty set
A is Element of the carrier of FMT
B is Element of the carrier of FMT
(FMT,A,B) is Element of BOOLEAN
y is Element of the carrier of C
z is Element of the carrier of C
(C,y,z) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^s is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( b₁ in B & (U_FT b₁) \ {b₁} misses B ) } is set
(FMT,A,B) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
{A} is non empty Element of bool the carrier of FMT
(U_FT A) \ {A} is Element of bool the carrier of FMT
((U_FT A) \ {A}) /\ B is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
(FMT,A,C) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
(FMT,A,C) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
{A} is non empty Element of bool the carrier of FMT
(U_FT A) \ {A} is Element of bool the carrier of FMT
((U_FT A) \ {A}) /\ B is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
(FMT,A,C) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
(FMT,A,C) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
(FMT,A,y) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^n is Element of bool the carrier of FMT
B ^s is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( b₁ in B & (U_FT b₁) \ {b₁} misses B ) } is set
B \ (B ^s) is Element of bool the carrier of FMT
(FMT,A,B) is Element of BOOLEAN
U_FT A is Element of bool the carrier of FMT
{A} is non empty Element of bool the carrier of FMT
(U_FT A) \ {A} is Element of bool the carrier of FMT
((U_FT A) \ {A}) /\ B is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C) is Element of BOOLEAN
(FMT,A,C,B) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
(FMT,A,C) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
(FMT,A,C) is Element of BOOLEAN
{A} is non empty Element of bool the carrier of FMT
U_FT A is Element of bool the carrier of FMT
(U_FT A) \ {A} is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,A,C,B) is Element of BOOLEAN
(FMT,A,C) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,A,y,B) is Element of BOOLEAN
(FMT,A,y) is Element of BOOLEAN
FMT is non empty RelStr
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
B is Element of bool the carrier of FMT
B ^f is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of the carrier of FMT st
( b₂ in B & b₁ in U_FT b₂ ) } is set
C is Element of the carrier of FMT
(FMT,C,B) is Element of BOOLEAN
(FMT,C,A) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,C,B) is Element of BOOLEAN
(FMT,C,A) is Element of BOOLEAN
U_FT C is Element of bool the carrier of FMT
C is Element of the carrier of FMT
U_FT C is Element of bool the carrier of FMT
(FMT,C,B) is Element of BOOLEAN
(FMT,C,A) is Element of BOOLEAN
C is Element of the carrier of FMT
(FMT,C,B) is Element of BOOLEAN
(FMT,C,A) is Element of BOOLEAN
y is Element of the carrier of FMT
(FMT,y,B) is Element of BOOLEAN
(FMT,y,A) is Element of BOOLEAN
the non empty set is non empty set
bool the non empty set is non empty set
bool (bool the non empty set ) is non empty set
[: the non empty set ,(bool (bool the non empty set )):] is non empty set
bool [: the non empty set ,(bool (bool the non empty set )):] is non empty set
the V7() V10( the non empty set ) V11( bool (bool the non empty set )) Function-like V18( the non empty set , bool (bool the non empty set )) Element of bool [: the non empty set ,(bool (bool the non empty set )):] is V7() V10( the non empty set ) V11( bool (bool the non empty set )) Function-like V18( the non empty set , bool (bool the non empty set )) Element of bool [: the non empty set ,(bool (bool the non empty set )):]
( the non empty set , the V7() V10( the non empty set ) V11( bool (bool the non empty set )) Function-like V18( the non empty set , bool (bool the non empty set )) Element of bool [: the non empty set ,(bool (bool the non empty set )):]) is () ()
the carrier of ( the non empty set , the V7() V10( the non empty set ) V11( bool (bool the non empty set )) Function-like V18( the non empty set , bool (bool the non empty set )) Element of bool [: the non empty set ,(bool (bool the non empty set )):]) is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
A is Element of the carrier of FMT
the of FMT . A is Element of bool (bool the carrier of FMT)
FMT is non empty TopStruct
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
the topology of FMT is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
{ b₁ where b₁ is Element of bool the carrier of FMT : ( b₁ in the topology of FMT & a₁ in b₁ ) } is set
A is Element of the carrier of FMT
{ b₁ where b₁ is Element of bool the carrier of FMT : ( b₁ in the topology of FMT & A in b₁ ) } is set
B is set
C is Element of bool the carrier of FMT
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
A is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
( the carrier of FMT,A) is () ()
B is non empty () ()
the carrier of B is non empty set
C is Element of the carrier of B
(B,C) is Element of bool (bool the carrier of B)
bool the carrier of B is non empty set
bool (bool the carrier of B) is non empty set
the of B is V7() V10( the carrier of B) V11( bool (bool the carrier of B)) Function-like V18( the carrier of B, bool (bool the carrier of B)) Element of bool [: the carrier of B,(bool (bool the carrier of B)):]
[: the carrier of B,(bool (bool the carrier of B)):] is non empty set
bool [: the carrier of B,(bool (bool the carrier of B)):] is non empty set
the of B . C is Element of bool (bool the carrier of B)
{ b₁ where b₁ is Element of bool the carrier of FMT : ( b₁ in the topology of FMT & C in b₁ ) } is set
A is non empty () ()
the carrier of A is non empty set
A is non empty () ()
the carrier of A is non empty set
B is non empty () ()
the carrier of B is non empty set
bool the carrier of B is non empty set
bool (bool the carrier of B) is non empty set
the of B is V7() V10( the carrier of B) V11( bool (bool the carrier of B)) Function-like V18( the carrier of B, bool (bool the carrier of B)) Element of bool [: the carrier of B,(bool (bool the carrier of B)):]
[: the carrier of B,(bool (bool the carrier of B)):] is non empty set
bool [: the carrier of B,(bool (bool the carrier of B)):] is non empty set
C is Element of the carrier of B
the of B . C is Element of bool (bool the carrier of B)
{ b₁ where b₁ is Element of bool the carrier of FMT : ( b₁ in the topology of FMT & C in b₁ ) } is set
(B,C) is Element of bool (bool the carrier of B)
bool the carrier of A is non empty set
bool (bool the carrier of A) is non empty set
the of A is V7() V10( the carrier of A) V11( bool (bool the carrier of A)) Function-like V18( the carrier of A, bool (bool the carrier of A)) Element of bool [: the carrier of A,(bool (bool the carrier of A)):]
[: the carrier of A,(bool (bool the carrier of A)):] is non empty set
bool [: the carrier of A,(bool (bool the carrier of A)):] is non empty set
C is Element of the carrier of A
the of A . C is Element of bool (bool the carrier of A)
{ b₁ where b₁ is Element of bool the carrier of FMT : ( b₁ in the topology of FMT & C in b₁ ) } is set
(A,C) is Element of bool (bool the carrier of A)
C is Element of the carrier of A
the of A . C is Element of bool (bool the carrier of A)
{ b₁ where b₁ is Element of bool the carrier of FMT : ( b₁ in the topology of FMT & C in b₁ ) } is set
the of B . C is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses A & not b<sub>2</sub> misses A ` ) ) } is set
{ b₁ where b₁ is Element of the carrier of FMT : S₁[b₁] } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
B ` is Element of bool the carrier of FMT
the carrier of FMT \ B is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses B & not b<sub>2</sub> misses B ` ) ) } is set
C is Element of bool the carrier of FMT
y is Element of the carrier of FMT
(FMT,y) is Element of bool (bool the carrier of FMT)
the of FMT . y is Element of bool (bool the carrier of FMT)
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
{ b₁ where b₁ is Element of the carrier of FMT : S₁[b₁] } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
C is Element of bool the carrier of FMT
y is Element of the carrier of FMT
(FMT,y) is Element of bool (bool the carrier of FMT)
the of FMT . y is Element of bool (bool the carrier of FMT)
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
{ b₁ where b₁ is Element of the carrier of FMT : S₁[b₁] } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
C is Element of the carrier of FMT
y is Element of bool the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
the of FMT . C is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( b₁ in A & ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ \ {b₁} misses A ) ) } is set
{ b₁ where b₁ is Element of the carrier of FMT : S₁[b₁] } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
{A} is non empty Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( b₁ in B & ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ \ {b₁} misses B ) ) } is set
C is Element of the carrier of FMT
y is Element of bool the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
the of FMT . C is Element of bool (bool the carrier of FMT)
{C} is non empty Element of bool the carrier of FMT
y \ {C} is Element of bool the carrier of FMT
C is Element of bool the carrier of FMT
C \ {A} is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( b₁ in A & ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ \ {b₁} misses A ) ) } is set
A \ (FMT,A) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
{A} is non empty Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( b₁ in B & ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ \ {b₁} misses B ) ) } is set
B \ (FMT,B) is Element of bool the carrier of FMT
C is Element of bool the carrier of FMT
C \ {A} is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
C is set
y is Element of the carrier of FMT
(FMT,y) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . y is Element of bool (bool the carrier of FMT)
z is Element of bool the carrier of FMT
z /\ B is Element of bool the carrier of FMT
W is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
C is set
y is Element of the carrier of FMT
(FMT,y) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . y is Element of bool (bool the carrier of FMT)
z is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
(FMT,A) \/ (FMT,B) is Element of bool the carrier of FMT
A \/ B is Element of bool the carrier of FMT
(FMT,(A \/ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A \/ B ) } is set
C is set
B \/ A is Element of bool the carrier of FMT
(FMT,(B \/ A)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B \/ A ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
B is Element of bool the carrier of FMT
A /\ B is Element of bool the carrier of FMT
(FMT,(A /\ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A /\ B ) } is set
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
(FMT,A) /\ (FMT,B) is Element of bool the carrier of FMT
C is set
B /\ A is Element of bool the carrier of FMT
(FMT,(B /\ A)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B /\ A ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
(FMT,A) \/ (FMT,B) is Element of bool the carrier of FMT
A \/ B is Element of bool the carrier of FMT
(FMT,(A \/ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A \/ B ) } is set
C is set
B \/ A is Element of bool the carrier of FMT
(FMT,(B \/ A)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B \/ A ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
B is Element of bool the carrier of FMT
A /\ B is Element of bool the carrier of FMT
(FMT,(A /\ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A /\ B ) } is set
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
(FMT,A) /\ (FMT,B) is Element of bool the carrier of FMT
C is set
B /\ A is Element of bool the carrier of FMT
(FMT,(B /\ A)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B /\ A ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A \/ B is Element of bool the carrier of FMT
(FMT,(A \/ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A \/ B ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
(FMT,A) \/ (FMT,B) is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
y /\ (A \/ B) is Element of bool the carrier of FMT
y /\ A is Element of bool the carrier of FMT
y /\ B is Element of bool the carrier of FMT
(y /\ A) \/ (y /\ B) is Element of bool the carrier of FMT
y is Element of bool the carrier of FMT
z is Element of bool the carrier of FMT
y /\ z is Element of bool the carrier of FMT
W is Element of bool the carrier of FMT
W /\ A is Element of bool the carrier of FMT
y /\ A is Element of bool the carrier of FMT
W /\ B is Element of bool the carrier of FMT
z /\ B is Element of bool the carrier of FMT
c₈ is Element of the carrier of FMT
c₉ is Element of the carrier of FMT
y is Element of bool the carrier of FMT
z is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
B /\ C is Element of bool the carrier of FMT
C ` is Element of bool the carrier of FMT
the carrier of FMT \ C is set
(FMT,(C `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses C ` ) } is set
B ` is Element of bool the carrier of FMT
the carrier of FMT \ B is set
(FMT,(B `)) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or not b<sub>2</sub> misses B ` ) } is set
(B `) \/ (C `) is Element of bool the carrier of FMT
(FMT,((B `) \/ (C `))) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses (B `) \/ (C `) ) } is set
(FMT,(B `)) \/ (FMT,(C `)) is Element of bool the carrier of FMT
y is Element of bool the carrier of FMT
(B /\ C) ` is Element of bool the carrier of FMT
the carrier of FMT \ (B /\ C) is set
y /\ ((B /\ C) `) is Element of bool the carrier of FMT
y \ (B /\ C) is Element of bool the carrier of FMT
y /\ ((B `) \/ (C `)) is Element of bool the carrier of FMT
A is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A \/ B is Element of bool the carrier of FMT
(FMT,(A \/ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A \/ B ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
(FMT,A) \/ (FMT,B) is Element of bool the carrier of FMT
y is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
z is Element of bool the carrier of FMT
y /\ z is Element of bool the carrier of FMT
W is Element of bool the carrier of FMT
c₈ is Element of bool the carrier of FMT
W \/ c₈ is Element of bool the carrier of FMT
(FMT,(W \/ c₈)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses W \/ c₈ ) } is set
(FMT,W) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses W ) } is set
(FMT,c₈) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses c₈ ) } is set
(FMT,W) \/ (FMT,c₈) is Element of bool the carrier of FMT
c₁₀ is Element of bool the carrier of FMT
c₉ is Element of the carrier of FMT
(FMT,c₉) is Element of bool (bool the carrier of FMT)
the of FMT . c₉ is Element of bool (bool the carrier of FMT)
c₁₁ is Element of bool the carrier of FMT
c₁₀ /\ c₁₁ is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
(FMT,A) /\ (FMT,B) is Element of bool the carrier of FMT
A /\ B is Element of bool the carrier of FMT
(FMT,(A /\ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A /\ B ) } is set
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
z is Element of bool the carrier of FMT
y is Element of bool the carrier of FMT
z is Element of bool the carrier of FMT
y /\ z is Element of bool the carrier of FMT
W is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
B /\ C is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
(FMT,C) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= C ) } is set
(FMT,B) /\ (FMT,C) is Element of bool the carrier of FMT
(FMT,(B /\ C)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B /\ C ) } is set
B is Element of bool the carrier of FMT
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
B /\ C is Element of bool the carrier of FMT
y is Element of bool the carrier of FMT
(FMT,y) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= y ) } is set
z is Element of bool the carrier of FMT
(FMT,z) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= z ) } is set
(FMT,y) /\ (FMT,z) is Element of bool the carrier of FMT
y /\ z is Element of bool the carrier of FMT
(FMT,(y /\ z)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= y /\ z ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A \/ B is Element of bool the carrier of FMT
(FMT,(A \/ B)) is Element of bool the carrier of FMT
(A \/ B) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A \/ B) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses A \/ B & not b<sub>2</sub> misses (A \/ B) ` ) ) } is set
(FMT,A) is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses A & not b<sub>2</sub> misses A ` ) ) } is set
(FMT,B) is Element of bool the carrier of FMT
B ` is Element of bool the carrier of FMT
the carrier of FMT \ B is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses B & not b<sub>2</sub> misses B ` ) ) } is set
(FMT,A) \/ (FMT,B) is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
y /\ ((A \/ B) `) is Element of bool the carrier of FMT
(A `) /\ (B `) is Element of bool the carrier of FMT
y /\ ((A `) /\ (B `)) is Element of bool the carrier of FMT
y /\ (A `) is Element of bool the carrier of FMT
(y /\ (A `)) /\ (B `) is Element of bool the carrier of FMT
y /\ (B `) is Element of bool the carrier of FMT
(y /\ (B `)) /\ (A `) is Element of bool the carrier of FMT
y /\ (A \/ B) is Element of bool the carrier of FMT
y /\ A is Element of bool the carrier of FMT
y /\ B is Element of bool the carrier of FMT
(y /\ A) \/ (y /\ B) is Element of bool the carrier of FMT
z is set
W is set
y is Element of bool the carrier of FMT
z is Element of bool the carrier of FMT
y /\ z is Element of bool the carrier of FMT
W is Element of bool the carrier of FMT
W /\ B is Element of bool the carrier of FMT
z /\ B is Element of bool the carrier of FMT
W /\ (B `) is Element of bool the carrier of FMT
z /\ (B `) is Element of bool the carrier of FMT
W /\ A is Element of bool the carrier of FMT
y /\ A is Element of bool the carrier of FMT
W /\ (A `) is Element of bool the carrier of FMT
y /\ (A `) is Element of bool the carrier of FMT
c<sub>8</sub> is set
c<sub>9</sub> is set
c<sub>8</sub> is set
c<sub>9</sub> is set
y is Element of bool the carrier of FMT
z is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
B is Element of bool the carrier of FMT
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
B /\ C is Element of bool the carrier of FMT
B ` is Element of bool the carrier of FMT
the carrier of FMT \ B is set
(FMT,(B `)) is Element of bool the carrier of FMT
(B `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (B `) is set
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or ( not b₂ misses B ` & not b<sub>2</sub> misses (B `) ` ) ) } is set
C ` is Element of bool the carrier of FMT
the carrier of FMT \ C is set
(B `) \/ (C `) is Element of bool the carrier of FMT
(FMT,((B `) \/ (C `))) is Element of bool the carrier of FMT
((B `) \/ (C `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((B `) \/ (C `)) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses (B `) \/ (C `) & not b<sub>2</sub> misses ((B `) \/ (C `)) ` ) ) } is set
(FMT,(C `)) is Element of bool the carrier of FMT
(C `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (C `) is set
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or ( not b₂ misses C ` & not b<sub>2</sub> misses (C `) ` ) ) } is set
(FMT,(B `)) \/ (FMT,(C `)) is Element of bool the carrier of FMT
y is Element of bool the carrier of FMT
(B /\ C) ` is Element of bool the carrier of FMT
the carrier of FMT \ (B /\ C) is set
y /\ ((B /\ C) `) is Element of bool the carrier of FMT
y \ (B /\ C) is Element of bool the carrier of FMT
((B /\ C) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((B /\ C) `) is set
y /\ (((B /\ C) `) `) is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
B /\ C is Element of bool the carrier of FMT
y is Element of bool the carrier of FMT
z is Element of bool the carrier of FMT
y \/ z is Element of bool the carrier of FMT
(FMT,(y \/ z)) is Element of bool the carrier of FMT
(y \/ z) ` is Element of bool the carrier of FMT
the carrier of FMT \ (y \/ z) is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses y \/ z & not b<sub>2</sub> misses (y \/ z) ` ) ) } is set
(FMT,y) is Element of bool the carrier of FMT
y ` is Element of bool the carrier of FMT
the carrier of FMT \ y is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses y & not b<sub>2</sub> misses y ` ) ) } is set
(FMT,z) is Element of bool the carrier of FMT
z ` is Element of bool the carrier of FMT
the carrier of FMT \ z is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses z & not b<sub>2</sub> misses z ` ) ) } is set
(FMT,y) \/ (FMT,z) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of the carrier of FMT
{A} is non empty Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ( b₁ in B & ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ \ {b₁} misses B ) ) } is set
B \ {A} is Element of bool the carrier of FMT
(FMT,(B \ {A})) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B \ {A} ) } is set
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
{A} ` is Element of bool the carrier of FMT
the carrier of FMT \ {A} is set
B /\ ({A} `) is Element of bool the carrier of FMT
C /\ (B /\ ({A} `)) is Element of bool the carrier of FMT
C /\ ({A} `) is Element of bool the carrier of FMT
(C /\ ({A} `)) /\ B is Element of bool the carrier of FMT
C \ {A} is Element of bool the carrier of FMT
(C \ {A}) /\ B is Element of bool the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
C \ {A} is Element of bool the carrier of FMT
{A} ` is Element of bool the carrier of FMT
the carrier of FMT \ {A} is set
C /\ ({A} `) is Element of bool the carrier of FMT
(C /\ ({A} `)) /\ B is Element of bool the carrier of FMT
({A} `) /\ B is Element of bool the carrier of FMT
C /\ (({A} `) /\ B) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
B is Element of bool the carrier of FMT
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
{A} is non empty Element of bool the carrier of FMT
C is set
(FMT,{A}) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses {A} ) } is set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
B is set
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
B is set
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A is Element of the carrier of FMT
(FMT,A) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . A is Element of bool (bool the carrier of FMT)
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
(FMT,(A `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ` ) } is set
(FMT,(A `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,(A `)) is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
B is set
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
y /\ (A `) is Element of bool the carrier of FMT
y \ A is Element of bool the carrier of FMT
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
y \ A is Element of bool the carrier of FMT
y /\ (A `) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
(FMT,(A `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ` ) } is set
(FMT,(A `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,(A `)) is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
B is set
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
z is set
C is Element of the carrier of FMT
(FMT,C) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . C is Element of bool (bool the carrier of FMT)
y is Element of bool the carrier of FMT
z is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses A & not b<sub>2</sub> misses A ` ) ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
(FMT,(A `)) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or not b<sub>2</sub> misses A ` ) } is set
(FMT,A) /\ (FMT,(A `)) is Element of bool the carrier of FMT
B is Element of the carrier of FMT
(FMT,B) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . B is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
C is Element of bool the carrier of FMT
(FMT,B) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . B is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or ( not b₂ misses A & not b₂ misses A ` ) ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or not b<sub>2</sub> misses A ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : ex b<sub>2</sub> being Element of bool the carrier of FMT st
( b<sub>2</sub> in (FMT,b<sub>1</sub>) & b<sub>2</sub> c= A ) } is set
(FMT,A) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,A) is set
(FMT,A) /\ ((FMT,A) `) is Element of bool the carrier of FMT
(FMT,(A `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ` ) } is set
(FMT,(A `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,(A `)) is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses A & not b<sub>2</sub> misses A ` ) ) } is set
(FMT,(A `)) is Element of bool the carrier of FMT
(A `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A `) is set
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or ( not b₂ misses A ` & not b<sub>2</sub> misses (A `) ` ) ) } is set
(FMT,((A `) `)) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or not b<sub>2</sub> misses (A `) ` ) } is set
(FMT,(A `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ` ) } is set
(FMT,((A `) `)) /\ (FMT,(A `)) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses A & not b<sub>2</sub> misses A ` ) ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
(FMT,A) \ (FMT,A) is Element of bool the carrier of FMT
B is set
(FMT,(A `)) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or not b<sub>2</sub> misses A ` ) } is set
(FMT,(A `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,(A `)) is set
((FMT,(A `)) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((FMT,(A `)) `) is set
(FMT,A) /\ (((FMT,(A `)) `) `) is Element of bool the carrier of FMT
(FMT,A) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,A) is set
(FMT,A) /\ ((FMT,A) `) is Element of bool the carrier of FMT
(FMT,A) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,A) is set
(FMT,A) /\ ((FMT,A) `) is Element of bool the carrier of FMT
(FMT,(A `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ` ) } is set
(FMT,(A `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,(A `)) is set
((FMT,(A `)) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((FMT,(A `)) `) is set
(FMT,A) /\ (((FMT,(A `)) `) `) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or ( not b<sub>2</sub> misses A & not b<sub>2</sub> misses A ` ) ) } is set
A /\ (FMT,A) is Element of bool the carrier of FMT
(A `) /\ (FMT,A) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or ( not b₂ misses A & not b₂ misses A ` ) ) } is set
(FMT,A) is Element of bool the carrier of FMT
A /\ (FMT,A) is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
(A `) /\ (FMT,A) is Element of bool the carrier of FMT
(FMT,A) \/ (FMT,A) is Element of bool the carrier of FMT
B is set
[#] the carrier of FMT is non empty non proper Element of bool the carrier of FMT
([#] the carrier of FMT) /\ (FMT,A) is Element of bool the carrier of FMT
A \/ (A `) is Element of bool the carrier of FMT
(A \/ (A `)) /\ (FMT,A) is Element of bool the carrier of FMT
A \/ (A `) is Element of bool the carrier of FMT
(A \/ (A `)) /\ (FMT,A) is Element of bool the carrier of FMT
[#] the carrier of FMT is non empty non proper Element of bool the carrier of FMT
([#] the carrier of FMT) /\ (FMT,A) is Element of bool the carrier of FMT
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
(FMT,(A `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ` ) } is set
(FMT,(A `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,(A `)) is set
((FMT,(A `)) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((FMT,(A `)) `) is set
(FMT,A) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : for b<sub>2</sub> being Element of bool the carrier of FMT holds
( not b<sub>2</sub> in (FMT,b<sub>1</sub>) or not b<sub>2</sub> misses A ) } is set
(FMT,A) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,A) is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
A ` is Element of bool the carrier of FMT
the carrier of FMT \ A is set
(FMT,(A `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ` ) } is set
(A `) ` is Element of bool the carrier of FMT
the carrier of FMT \ (A `) is set
(FMT,((A `) `)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= (A `) ` ) } is set
(FMT,((A `) `)) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,((A `) `)) is set
(FMT,A) is Element of bool the carrier of FMT
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of FMT : ex b<sub>2</sub> being Element of bool the carrier of FMT st
( b<sub>2</sub> in (FMT,b<sub>1</sub>) & b<sub>2</sub> c= A ) } is set
(FMT,A) ` is Element of bool the carrier of FMT
the carrier of FMT \ (FMT,A) is set
((FMT,A) `) ` is Element of bool the carrier of FMT
the carrier of FMT \ ((FMT,A) `) is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
B is Element of bool the carrier of FMT
A /\ B is Element of bool the carrier of FMT
(FMT,(A /\ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A /\ B ) } is set
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses A ) } is set
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses B ) } is set
(FMT,A) /\ (FMT,B) is Element of bool the carrier of FMT
C is Element of bool the carrier of FMT
(FMT,C) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses C ) } is set
y is Element of the carrier of FMT
{y} is non empty Element of bool the carrier of FMT
(FMT,y) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . y is Element of bool (bool the carrier of FMT)
z is set
C is Element of bool the carrier of FMT
(FMT,C) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : for b₂ being Element of bool the carrier of FMT holds
( not b₂ in (FMT,b₁) or not b₂ misses C ) } is set
FMT is non empty ()
the carrier of FMT is non empty set
bool the carrier of FMT is non empty set
A is Element of bool the carrier of FMT
(FMT,A) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A ) } is set
B is Element of bool the carrier of FMT
(FMT,B) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= B ) } is set
(FMT,A) \/ (FMT,B) is Element of bool the carrier of FMT
A \/ B is Element of bool the carrier of FMT
(FMT,(A \/ B)) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= A \/ B ) } is set
C is Element of bool the carrier of FMT
(FMT,C) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= C ) } is set
y is Element of the carrier of FMT
{y} is non empty Element of bool the carrier of FMT
bool C is non empty set
(FMT,y) is Element of bool (bool the carrier of FMT)
bool (bool the carrier of FMT) is non empty set
the of FMT is V7() V10( the carrier of FMT) V11( bool (bool the carrier of FMT)) Function-like V18( the carrier of FMT, bool (bool the carrier of FMT)) Element of bool [: the carrier of FMT,(bool (bool the carrier of FMT)):]
[: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
bool [: the carrier of FMT,(bool (bool the carrier of FMT)):] is non empty set
the of FMT . y is Element of bool (bool the carrier of FMT)
C is Element of bool the carrier of FMT
(FMT,C) is Element of bool the carrier of FMT
{ b₁ where b₁ is Element of the carrier of FMT : ex b₂ being Element of bool the carrier of FMT st
( b₂ in (FMT,b₁) & b₂ c= C ) } is set