:: BVFUNC_1 semantic presentation

NAT is Element of bool REAL
REAL is set
bool REAL is non empty set
COMPLEX is set
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is non empty set
NAT is set
bool NAT is non empty set
bool NAT is non empty set
BOOLEAN is non empty set
0 is Element of NAT
the empty Function-like functional V62() set is empty Function-like functional V62() set
1 is non empty set
{0,1} is set
{} is set
TRUE is ext-real V10() V43() V44() boolean Element of BOOLEAN
FALSE is ext-real V10() V43() V44() boolean Element of BOOLEAN
FALSE is ext-real V10() V43() V44() boolean set
TRUE is ext-real V10() V43() V44() boolean set
x is ext-real V10() V43() V44() boolean set
y is ext-real V10() V43() V44() boolean set
x => y is ext-real V10() V43() V44() boolean set
'not' x is ext-real V10() V43() V44() boolean set
K134(1,x) is set
('not' x) 'or' y is ext-real V10() V43() V44() boolean set
'not' ('not' x) is ext-real V10() V43() V44() boolean set
K134(1,('not' x)) is set
'not' y is ext-real V10() V43() V44() boolean set
K134(1,y) is set
('not' ('not' x)) '&' ('not' y) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' x)),('not' y)) is ext-real V10() V44() set
'not' (('not' ('not' x)) '&' ('not' y)) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' x)) '&' ('not' y))) is set
F₁() is non empty set
[:F₁(),BOOLEAN:] is non empty set
bool [:F₁(),BOOLEAN:] is non empty set
x is non empty Relation-like F₁() -defined BOOLEAN -valued Function-like V21(F₁()) quasi_total boolean-valued Element of bool [:F₁(),BOOLEAN:]
y is non empty Relation-like F₁() -defined BOOLEAN -valued Function-like V21(F₁()) quasi_total boolean-valued Element of bool [:F₁(),BOOLEAN:]
z is Element of F₁()
x . z is ext-real V10() V43() V44() boolean set
y . z is ext-real V10() V43() V44() boolean set
y . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
F₂(z) is set
x . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
'not' y is Relation-like Function-like boolean-valued set
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
'not' z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
y '&' z is Relation-like Function-like boolean-valued set
C is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
D is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
C '&' D is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
x is Relation-like Function-like boolean-valued set
dom x is set
y is Relation-like Function-like boolean-valued set
dom y is set
(dom x) /\ (dom y) is set
z is Relation-like Function-like set
dom z is set
C is set
rng z is set
D is set
z . D is set
x . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
(x . D) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' (x . D) is ext-real V10() V43() V44() boolean set
K134(1,(x . D)) is set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (x . D)) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' (x . D)),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' (x . D)) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' (x . D)) '&' ('not' (y . D)))) is set
z is Relation-like Function-like boolean-valued set
dom z is set
C is Relation-like Function-like boolean-valued set
dom C is set
D is set
z . D is ext-real V10() V43() V44() boolean set
C . D is ext-real V10() V43() V44() boolean set
x . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
(x . D) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' (x . D) is ext-real V10() V43() V44() boolean set
K134(1,(x . D)) is set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (x . D)) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' (x . D)),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' (x . D)) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' (x . D)) '&' ('not' (y . D)))) is set
z is Relation-like Function-like boolean-valued set
dom z is set
C is Relation-like Function-like boolean-valued set
dom C is set
D is Relation-like Function-like boolean-valued set
dom D is set
(dom C) /\ (dom D) is set
(dom D) /\ (dom C) is set
g is set
z . g is ext-real V10() V43() V44() boolean set
D . g is ext-real V10() V43() V44() boolean set
C . g is ext-real V10() V43() V44() boolean set
(D . g) 'or' (C . g) is ext-real V10() V43() V44() boolean set
'not' (D . g) is ext-real V10() V43() V44() boolean set
K134(1,(D . g)) is set
'not' (C . g) is ext-real V10() V43() V44() boolean set
K134(1,(C . g)) is set
('not' (D . g)) '&' ('not' (C . g)) is ext-real V10() V43() V44() boolean set
K131(('not' (D . g)),('not' (C . g))) is ext-real V10() V44() set
'not' (('not' (D . g)) '&' ('not' (C . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' (D . g)) '&' ('not' (C . g)))) is set
z is Relation-like Function-like boolean-valued set
dom z is set
(dom z) /\ (dom z) is set
D is set
C is Relation-like Function-like boolean-valued set
dom C is set
C . D is ext-real V10() V43() V44() boolean set
(C . D) 'or' (C . D) is ext-real V10() V43() V44() boolean set
'not' (C . D) is ext-real V10() V43() V44() boolean set
K134(1,(C . D)) is set
('not' (C . D)) '&' ('not' (C . D)) is ext-real V10() V43() V44() boolean set
K131(('not' (C . D)),('not' (C . D))) is ext-real V10() V44() set
'not' (('not' (C . D)) '&' ('not' (C . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' (C . D)) '&' ('not' (C . D)))) is set
z is Relation-like Function-like set
dom z is set
C is set
z . C is set
x . C is ext-real V10() V43() V44() boolean set
y . C is ext-real V10() V43() V44() boolean set
(x . C) 'xor' (y . C) is ext-real V10() V43() V44() boolean set
(x . C) <=> (y . C) is ext-real V10() V43() V44() boolean set
(x . C) => (y . C) is ext-real V10() V43() V44() boolean set
'not' (x . C) is ext-real V10() V43() V44() boolean set
K134(1,(x . C)) is set
('not' (x . C)) 'or' (y . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . C))) is set
'not' (y . C) is ext-real V10() V43() V44() boolean set
K134(1,(y . C)) is set
('not' ('not' (x . C))) '&' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . C))),('not' (y . C))) is ext-real V10() V44() set
'not' (('not' ('not' (x . C))) '&' ('not' (y . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . C))) '&' ('not' (y . C)))) is set
(y . C) => (x . C) is ext-real V10() V43() V44() boolean set
('not' (y . C)) 'or' (x . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . C))) is set
('not' ('not' (y . C))) '&' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . C))),('not' (x . C))) is ext-real V10() V44() set
'not' (('not' ('not' (y . C))) '&' ('not' (x . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . C))) '&' ('not' (x . C)))) is set
((x . C) => (y . C)) '&' ((y . C) => (x . C)) is ext-real V10() V43() V44() boolean set
K131(((x . C) => (y . C)),((y . C) => (x . C))) is ext-real V10() V44() set
'not' ((x . C) <=> (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,((x . C) <=> (y . C))) is set
z is Relation-like Function-like set
dom z is set
C is Relation-like Function-like set
dom C is set
D is set
z . D is set
C . D is set
x . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
(x . D) 'xor' (y . D) is ext-real V10() V43() V44() boolean set
(x . D) <=> (y . D) is ext-real V10() V43() V44() boolean set
(x . D) => (y . D) is ext-real V10() V43() V44() boolean set
'not' (x . D) is ext-real V10() V43() V44() boolean set
K134(1,(x . D)) is set
('not' (x . D)) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . D))) is set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' ('not' (x . D))) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . D))),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' ('not' (x . D))) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . D))) '&' ('not' (y . D)))) is set
(y . D) => (x . D) is ext-real V10() V43() V44() boolean set
('not' (y . D)) 'or' (x . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
('not' ('not' (y . D))) '&' ('not' (x . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (x . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (x . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (x . D)))) is set
((x . D) => (y . D)) '&' ((y . D) => (x . D)) is ext-real V10() V43() V44() boolean set
K131(((x . D) => (y . D)),((y . D) => (x . D))) is ext-real V10() V44() set
'not' ((x . D) <=> (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,((x . D) <=> (y . D))) is set
z is Relation-like Function-like set
dom z is set
C is Relation-like Function-like boolean-valued set
dom C is set
D is Relation-like Function-like boolean-valued set
dom D is set
(dom C) /\ (dom D) is set
(dom D) /\ (dom C) is set
g is set
z . g is set
D . g is ext-real V10() V43() V44() boolean set
C . g is ext-real V10() V43() V44() boolean set
(D . g) 'xor' (C . g) is ext-real V10() V43() V44() boolean set
(D . g) <=> (C . g) is ext-real V10() V43() V44() boolean set
(D . g) => (C . g) is ext-real V10() V43() V44() boolean set
'not' (D . g) is ext-real V10() V43() V44() boolean set
K134(1,(D . g)) is set
('not' (D . g)) 'or' (C . g) is ext-real V10() V43() V44() boolean set
'not' ('not' (D . g)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (D . g))) is set
'not' (C . g) is ext-real V10() V43() V44() boolean set
K134(1,(C . g)) is set
('not' ('not' (D . g))) '&' ('not' (C . g)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (D . g))),('not' (C . g))) is ext-real V10() V44() set
'not' (('not' ('not' (D . g))) '&' ('not' (C . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (D . g))) '&' ('not' (C . g)))) is set
(C . g) => (D . g) is ext-real V10() V43() V44() boolean set
('not' (C . g)) 'or' (D . g) is ext-real V10() V43() V44() boolean set
'not' ('not' (C . g)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (C . g))) is set
('not' ('not' (C . g))) '&' ('not' (D . g)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (C . g))),('not' (D . g))) is ext-real V10() V44() set
'not' (('not' ('not' (C . g))) '&' ('not' (D . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (C . g))) '&' ('not' (D . g)))) is set
((D . g) => (C . g)) '&' ((C . g) => (D . g)) is ext-real V10() V43() V44() boolean set
K131(((D . g) => (C . g)),((C . g) => (D . g))) is ext-real V10() V44() set
'not' ((D . g) <=> (C . g)) is ext-real V10() V43() V44() boolean set
K134(1,((D . g) <=> (C . g))) is set
x is Relation-like Function-like boolean-valued set
y is Relation-like Function-like boolean-valued set
(x,y) is Relation-like Function-like set
z is set
rng (x,y) is set
dom (x,y) is set
C is set
(x,y) . C is set
x . C is ext-real V10() V43() V44() boolean set
y . C is ext-real V10() V43() V44() boolean set
(x . C) 'xor' (y . C) is ext-real V10() V43() V44() boolean set
(x . C) <=> (y . C) is ext-real V10() V43() V44() boolean set
(x . C) => (y . C) is ext-real V10() V43() V44() boolean set
'not' (x . C) is ext-real V10() V43() V44() boolean set
K134(1,(x . C)) is set
('not' (x . C)) 'or' (y . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . C))) is set
'not' (y . C) is ext-real V10() V43() V44() boolean set
K134(1,(y . C)) is set
('not' ('not' (x . C))) '&' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . C))),('not' (y . C))) is ext-real V10() V44() set
'not' (('not' ('not' (x . C))) '&' ('not' (y . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . C))) '&' ('not' (y . C)))) is set
(y . C) => (x . C) is ext-real V10() V43() V44() boolean set
('not' (y . C)) 'or' (x . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . C))) is set
('not' ('not' (y . C))) '&' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . C))),('not' (x . C))) is ext-real V10() V44() set
'not' (('not' ('not' (y . C))) '&' ('not' (x . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . C))) '&' ('not' (x . C)))) is set
((x . C) => (y . C)) '&' ((y . C) => (x . C)) is ext-real V10() V43() V44() boolean set
K131(((x . C) => (y . C)),((y . C) => (x . C))) is ext-real V10() V44() set
'not' ((x . C) <=> (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,((x . C) <=> (y . C))) is set
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(y,z) is Relation-like Function-like boolean-valued set
dom y is set
dom z is set
dom (y,z) is set
x /\ x is set
rng (y,z) is set
C is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
dom C is set
dom y is set
dom z is set
dom (y,z) is set
x /\ x is set
D is Element of x
C . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
z . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . D) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' (y . D)) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' (y . D)),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' (y . D)) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' (y . D)) '&' ('not' (z . D)))) is set
(dom y) /\ (dom z) is set
D is set
C . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
z . D is ext-real V10() V43() V44() boolean set
(y . D) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' (y . D)) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' (y . D)),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' (y . D)) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' (y . D)) '&' ('not' (z . D)))) is set
(y,z) is Relation-like Function-like boolean-valued set
dom y is set
dom z is set
dom (y,z) is set
x /\ x is set
rng (y,z) is set
C is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
dom C is set
dom y is set
dom z is set
dom (y,z) is set
x /\ x is set
D is Element of x
C . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
z . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . D) 'xor' (z . D) is ext-real V10() V43() V44() boolean set
(y . D) <=> (z . D) is ext-real V10() V43() V44() boolean set
(y . D) => (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (y . D)) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' ('not' (y . D))) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (z . D)))) is set
(z . D) => (y . D) is ext-real V10() V43() V44() boolean set
('not' (z . D)) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (z . D))) is set
('not' ('not' (z . D))) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (z . D))),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' ('not' (z . D))) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (z . D))) '&' ('not' (y . D)))) is set
((y . D) => (z . D)) '&' ((z . D) => (y . D)) is ext-real V10() V43() V44() boolean set
K131(((y . D) => (z . D)),((z . D) => (y . D))) is ext-real V10() V44() set
'not' ((y . D) <=> (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,((y . D) <=> (z . D))) is set
(dom y) /\ (dom z) is set
D is set
C . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
z . D is ext-real V10() V43() V44() boolean set
(y . D) 'xor' (z . D) is ext-real V10() V43() V44() boolean set
(y . D) <=> (z . D) is ext-real V10() V43() V44() boolean set
(y . D) => (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (y . D)) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' ('not' (y . D))) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (z . D)))) is set
(z . D) => (y . D) is ext-real V10() V43() V44() boolean set
('not' (z . D)) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (z . D))) is set
('not' ('not' (z . D))) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (z . D))),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' ('not' (z . D))) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (z . D))) '&' ('not' (y . D)))) is set
((y . D) => (z . D)) '&' ((z . D) => (y . D)) is ext-real V10() V43() V44() boolean set
K131(((y . D) => (z . D)),((z . D) => (y . D))) is ext-real V10() V44() set
'not' ((y . D) <=> (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,((y . D) <=> (z . D))) is set
x is Relation-like Function-like boolean-valued set
dom x is set
y is Relation-like Function-like boolean-valued set
dom y is set
(dom x) /\ (dom y) is set
z is Relation-like Function-like set
dom z is set
C is set
z . C is set
x . C is ext-real V10() V43() V44() boolean set
y . C is ext-real V10() V43() V44() boolean set
(x . C) => (y . C) is ext-real V10() V43() V44() boolean set
'not' (x . C) is ext-real V10() V43() V44() boolean set
K134(1,(x . C)) is set
('not' (x . C)) 'or' (y . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . C))) is set
'not' (y . C) is ext-real V10() V43() V44() boolean set
K134(1,(y . C)) is set
('not' ('not' (x . C))) '&' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . C))),('not' (y . C))) is ext-real V10() V44() set
'not' (('not' ('not' (x . C))) '&' ('not' (y . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . C))) '&' ('not' (y . C)))) is set
z is Relation-like Function-like set
dom z is set
C is Relation-like Function-like set
dom C is set
D is set
z . D is set
C . D is set
x . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
(x . D) => (y . D) is ext-real V10() V43() V44() boolean set
'not' (x . D) is ext-real V10() V43() V44() boolean set
K134(1,(x . D)) is set
('not' (x . D)) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . D))) is set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' ('not' (x . D))) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . D))),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' ('not' (x . D))) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . D))) '&' ('not' (y . D)))) is set
z is Relation-like Function-like set
dom z is set
C is set
z . C is set
x . C is ext-real V10() V43() V44() boolean set
y . C is ext-real V10() V43() V44() boolean set
(x . C) <=> (y . C) is ext-real V10() V43() V44() boolean set
(x . C) => (y . C) is ext-real V10() V43() V44() boolean set
'not' (x . C) is ext-real V10() V43() V44() boolean set
K134(1,(x . C)) is set
('not' (x . C)) 'or' (y . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . C))) is set
'not' (y . C) is ext-real V10() V43() V44() boolean set
K134(1,(y . C)) is set
('not' ('not' (x . C))) '&' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . C))),('not' (y . C))) is ext-real V10() V44() set
'not' (('not' ('not' (x . C))) '&' ('not' (y . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . C))) '&' ('not' (y . C)))) is set
(y . C) => (x . C) is ext-real V10() V43() V44() boolean set
('not' (y . C)) 'or' (x . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . C))) is set
('not' ('not' (y . C))) '&' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . C))),('not' (x . C))) is ext-real V10() V44() set
'not' (('not' ('not' (y . C))) '&' ('not' (x . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . C))) '&' ('not' (x . C)))) is set
((x . C) => (y . C)) '&' ((y . C) => (x . C)) is ext-real V10() V43() V44() boolean set
K131(((x . C) => (y . C)),((y . C) => (x . C))) is ext-real V10() V44() set
z is Relation-like Function-like set
dom z is set
C is Relation-like Function-like set
dom C is set
D is set
z . D is set
C . D is set
x . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
(x . D) <=> (y . D) is ext-real V10() V43() V44() boolean set
(x . D) => (y . D) is ext-real V10() V43() V44() boolean set
'not' (x . D) is ext-real V10() V43() V44() boolean set
K134(1,(x . D)) is set
('not' (x . D)) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . D))) is set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' ('not' (x . D))) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . D))),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' ('not' (x . D))) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . D))) '&' ('not' (y . D)))) is set
(y . D) => (x . D) is ext-real V10() V43() V44() boolean set
('not' (y . D)) 'or' (x . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
('not' ('not' (y . D))) '&' ('not' (x . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (x . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (x . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (x . D)))) is set
((x . D) => (y . D)) '&' ((y . D) => (x . D)) is ext-real V10() V43() V44() boolean set
K131(((x . D) => (y . D)),((y . D) => (x . D))) is ext-real V10() V44() set
z is Relation-like Function-like set
dom z is set
C is Relation-like Function-like boolean-valued set
dom C is set
D is Relation-like Function-like boolean-valued set
dom D is set
(dom C) /\ (dom D) is set
(dom D) /\ (dom C) is set
g is set
z . g is set
D . g is ext-real V10() V43() V44() boolean set
C . g is ext-real V10() V43() V44() boolean set
(D . g) <=> (C . g) is ext-real V10() V43() V44() boolean set
(D . g) => (C . g) is ext-real V10() V43() V44() boolean set
'not' (D . g) is ext-real V10() V43() V44() boolean set
K134(1,(D . g)) is set
('not' (D . g)) 'or' (C . g) is ext-real V10() V43() V44() boolean set
'not' ('not' (D . g)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (D . g))) is set
'not' (C . g) is ext-real V10() V43() V44() boolean set
K134(1,(C . g)) is set
('not' ('not' (D . g))) '&' ('not' (C . g)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (D . g))),('not' (C . g))) is ext-real V10() V44() set
'not' (('not' ('not' (D . g))) '&' ('not' (C . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (D . g))) '&' ('not' (C . g)))) is set
(C . g) => (D . g) is ext-real V10() V43() V44() boolean set
('not' (C . g)) 'or' (D . g) is ext-real V10() V43() V44() boolean set
'not' ('not' (C . g)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (C . g))) is set
('not' ('not' (C . g))) '&' ('not' (D . g)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (C . g))),('not' (D . g))) is ext-real V10() V44() set
'not' (('not' ('not' (C . g))) '&' ('not' (D . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (C . g))) '&' ('not' (D . g)))) is set
((D . g) => (C . g)) '&' ((C . g) => (D . g)) is ext-real V10() V43() V44() boolean set
K131(((D . g) => (C . g)),((C . g) => (D . g))) is ext-real V10() V44() set
x is Relation-like Function-like boolean-valued set
y is Relation-like Function-like boolean-valued set
(x,y) is Relation-like Function-like set
z is set
rng (x,y) is set
dom (x,y) is set
C is set
(x,y) . C is set
x . C is ext-real V10() V43() V44() boolean set
y . C is ext-real V10() V43() V44() boolean set
(x . C) => (y . C) is ext-real V10() V43() V44() boolean set
'not' (x . C) is ext-real V10() V43() V44() boolean set
K134(1,(x . C)) is set
('not' (x . C)) 'or' (y . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . C))) is set
'not' (y . C) is ext-real V10() V43() V44() boolean set
K134(1,(y . C)) is set
('not' ('not' (x . C))) '&' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . C))),('not' (y . C))) is ext-real V10() V44() set
'not' (('not' ('not' (x . C))) '&' ('not' (y . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . C))) '&' ('not' (y . C)))) is set
(x,y) is Relation-like Function-like set
z is set
rng (x,y) is set
dom (x,y) is set
C is set
(x,y) . C is set
x . C is ext-real V10() V43() V44() boolean set
y . C is ext-real V10() V43() V44() boolean set
(x . C) 'xor' (y . C) is ext-real V10() V43() V44() boolean set
(x . C) <=> (y . C) is ext-real V10() V43() V44() boolean set
(x . C) => (y . C) is ext-real V10() V43() V44() boolean set
'not' (x . C) is ext-real V10() V43() V44() boolean set
K134(1,(x . C)) is set
('not' (x . C)) 'or' (y . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (x . C))) is set
'not' (y . C) is ext-real V10() V43() V44() boolean set
K134(1,(y . C)) is set
('not' ('not' (x . C))) '&' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (x . C))),('not' (y . C))) is ext-real V10() V44() set
'not' (('not' ('not' (x . C))) '&' ('not' (y . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (x . C))) '&' ('not' (y . C)))) is set
(y . C) => (x . C) is ext-real V10() V43() V44() boolean set
('not' (y . C)) 'or' (x . C) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . C))) is set
('not' ('not' (y . C))) '&' ('not' (x . C)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . C))),('not' (x . C))) is ext-real V10() V44() set
'not' (('not' ('not' (y . C))) '&' ('not' (x . C))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . C))) '&' ('not' (x . C)))) is set
((x . C) => (y . C)) '&' ((y . C) => (x . C)) is ext-real V10() V43() V44() boolean set
K131(((x . C) => (y . C)),((y . C) => (x . C))) is ext-real V10() V44() set
'not' ((x . C) <=> (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,((x . C) <=> (y . C))) is set
'not' ((x . C) 'xor' (y . C)) is ext-real V10() V43() V44() boolean set
K134(1,((x . C) 'xor' (y . C))) is set
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(y,z) is Relation-like Function-like boolean-valued set
dom y is set
dom z is set
dom (y,z) is set
x /\ x is set
rng (y,z) is set
C is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
dom z is set
dom y is set
dom (y,z) is set
x /\ x is set
D is Element of x
C . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
z . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . D) => (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (y . D)) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' ('not' (y . D))) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (z . D)))) is set
'not' (y . D) is ext-real V10() V43() V44() boolean Element of BOOLEAN
('not' (y . D)) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
('not' ('not' (y . D))) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (z . D)))) is set
dom C is set
D is set
C . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
z . D is ext-real V10() V43() V44() boolean set
(y . D) => (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (y . D)) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' ('not' (y . D))) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (z . D)))) is set
g is Element of x
C . g is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . g is ext-real V10() V43() V44() boolean Element of BOOLEAN
'not' (y . g) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K134(1,(y . g)) is set
z . g is ext-real V10() V43() V44() boolean Element of BOOLEAN
('not' (y . g)) 'or' (z . g) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . g)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . g))) is set
'not' (z . g) is ext-real V10() V43() V44() boolean set
K134(1,(z . g)) is set
('not' ('not' (y . g))) '&' ('not' (z . g)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . g))),('not' (z . g))) is ext-real V10() V44() set
'not' (('not' ('not' (y . g))) '&' ('not' (z . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . g))) '&' ('not' (z . g)))) is set
(dom y) /\ (dom z) is set
(y,z) is Relation-like Function-like boolean-valued set
dom y is set
dom z is set
dom (y,z) is set
x /\ x is set
rng (y,z) is set
C is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
dom z is set
dom y is set
dom (y,z) is set
x /\ x is set
D is Element of x
C . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
z . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . D) 'xor' (z . D) is ext-real V10() V43() V44() boolean set
(y . D) <=> (z . D) is ext-real V10() V43() V44() boolean set
(y . D) => (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (y . D)) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' ('not' (y . D))) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (z . D)))) is set
(z . D) => (y . D) is ext-real V10() V43() V44() boolean set
('not' (z . D)) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (z . D))) is set
('not' ('not' (z . D))) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (z . D))),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' ('not' (z . D))) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (z . D))) '&' ('not' (y . D)))) is set
((y . D) => (z . D)) '&' ((z . D) => (y . D)) is ext-real V10() V43() V44() boolean set
K131(((y . D) => (z . D)),((z . D) => (y . D))) is ext-real V10() V44() set
'not' ((y . D) <=> (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,((y . D) <=> (z . D))) is set
'not' ((y . D) 'xor' (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,((y . D) 'xor' (z . D))) is set
dom C is set
D is set
C . D is ext-real V10() V43() V44() boolean set
y . D is ext-real V10() V43() V44() boolean set
z . D is ext-real V10() V43() V44() boolean set
(y . D) <=> (z . D) is ext-real V10() V43() V44() boolean set
(y . D) => (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
('not' (y . D)) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . D))) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' ('not' (y . D))) '&' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . D))),('not' (z . D))) is ext-real V10() V44() set
'not' (('not' ('not' (y . D))) '&' ('not' (z . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . D))) '&' ('not' (z . D)))) is set
(z . D) => (y . D) is ext-real V10() V43() V44() boolean set
('not' (z . D)) 'or' (y . D) is ext-real V10() V43() V44() boolean set
'not' ('not' (z . D)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (z . D))) is set
('not' ('not' (z . D))) '&' ('not' (y . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (z . D))),('not' (y . D))) is ext-real V10() V44() set
'not' (('not' ('not' (z . D))) '&' ('not' (y . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (z . D))) '&' ('not' (y . D)))) is set
((y . D) => (z . D)) '&' ((z . D) => (y . D)) is ext-real V10() V43() V44() boolean set
K131(((y . D) => (z . D)),((z . D) => (y . D))) is ext-real V10() V44() set
g is Element of x
C . g is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . g is ext-real V10() V43() V44() boolean Element of BOOLEAN
z . g is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . g) 'xor' (z . g) is ext-real V10() V43() V44() boolean set
(y . g) <=> (z . g) is ext-real V10() V43() V44() boolean set
(y . g) => (z . g) is ext-real V10() V43() V44() boolean set
'not' (y . g) is ext-real V10() V43() V44() boolean set
K134(1,(y . g)) is set
('not' (y . g)) 'or' (z . g) is ext-real V10() V43() V44() boolean set
'not' ('not' (y . g)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (y . g))) is set
'not' (z . g) is ext-real V10() V43() V44() boolean set
K134(1,(z . g)) is set
('not' ('not' (y . g))) '&' ('not' (z . g)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (y . g))),('not' (z . g))) is ext-real V10() V44() set
'not' (('not' ('not' (y . g))) '&' ('not' (z . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (y . g))) '&' ('not' (z . g)))) is set
(z . g) => (y . g) is ext-real V10() V43() V44() boolean set
('not' (z . g)) 'or' (y . g) is ext-real V10() V43() V44() boolean set
'not' ('not' (z . g)) is ext-real V10() V43() V44() boolean set
K134(1,('not' (z . g))) is set
('not' ('not' (z . g))) '&' ('not' (y . g)) is ext-real V10() V43() V44() boolean set
K131(('not' ('not' (z . g))),('not' (y . g))) is ext-real V10() V44() set
'not' (('not' ('not' (z . g))) '&' ('not' (y . g))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ('not' (z . g))) '&' ('not' (y . g)))) is set
((y . g) => (z . g)) '&' ((z . g) => (y . g)) is ext-real V10() V43() V44() boolean set
K131(((y . g) => (z . g)),((z . g) => (y . g))) is ext-real V10() V44() set
'not' ((y . g) <=> (z . g)) is ext-real V10() V43() V44() boolean set
K134(1,((y . g) <=> (z . g))) is set
'not' ((y . g) 'xor' (z . g)) is ext-real V10() V43() V44() boolean set
K134(1,((y . g) 'xor' (z . g))) is set
(dom y) /\ (dom z) is set
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
x --> FALSE is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
C is Element of x
z . C is ext-real V10() V43() V44() boolean Element of BOOLEAN
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
x --> TRUE is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
C is Element of x
z . C is ext-real V10() V43() V44() boolean Element of BOOLEAN
x is non empty set
(x) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
(x,(x)) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,(x)) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
y is Element of x
(x,(x)) . y is ext-real V10() V43() V44() boolean Element of BOOLEAN
(x) . y is ext-real V10() V43() V44() boolean Element of BOOLEAN
'not' ((x) . y) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K134(1,((x) . y)) is set
y is Element of x
(x,(x)) . y is ext-real V10() V43() V44() boolean Element of BOOLEAN
(x) . y is ext-real V10() V43() V44() boolean Element of BOOLEAN
'not' ((x) . y) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K134(1,((x) . y)) is set
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,y) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,z) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
C is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,(x,y,z),C) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,z,C) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,(x,z,C)) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
D is Element of x
(x,(x,y,z),C) . D is ext-real V10() V43() V44() boolean set
(x,y,(x,z,C)) . D is ext-real V10() V43() V44() boolean set
(x,(x,y,z),C) . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(x,y,z) . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
C . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
((x,y,z) . D) '&' (C . D) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131(((x,y,z) . D),(C . D)) is ext-real V10() V44() set
y . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
z . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . D) '&' (z . D) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((y . D),(z . D)) is ext-real V10() V44() set
((y . D) '&' (z . D)) '&' (C . D) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131(((y . D) '&' (z . D)),(C . D)) is ext-real V10() V44() set
(z . D) '&' (C . D) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((z . D),(C . D)) is ext-real V10() V44() set
(y . D) '&' ((z . D) '&' (C . D)) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((y . D),((z . D) '&' (C . D))) is ext-real V10() V44() set
(x,z,C) . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . D) '&' ((x,z,C) . D) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((y . D),((x,z,C) . D)) is ext-real V10() V44() set
(x,y,(x,z,C)) . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
(x) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,(x)) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is Element of x
(x,y,(x)) . z is ext-real V10() V43() V44() boolean set
(x) . z is ext-real V10() V43() V44() boolean set
(x,y,(x)) . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
(x) . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . z) '&' ((x) . z) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((y . z),((x) . z)) is ext-real V10() V44() set
(y . z) '&' FALSE is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((y . z),FALSE) is ext-real V10() V44() set
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
(x) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,(x)) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is Element of x
(x,y,(x)) . z is ext-real V10() V43() V44() boolean set
y . z is ext-real V10() V43() V44() boolean set
(x,y,(x)) . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
y . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
(x) . z is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . z) '&' ((x) . z) is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((y . z),((x) . z)) is ext-real V10() V44() set
(y . z) '&' TRUE is ext-real V10() V43() V44() boolean Element of BOOLEAN
K131((y . z),TRUE) is ext-real V10() V44() set
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,y) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
x is non empty set
[:x,BOOLEAN:] is non empty set
bool [:x,BOOLEAN:] is non empty set
y is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
z is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,z) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
C is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,(x,y,z),C) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,z,C) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
(x,y,(x,z,C)) is non empty Relation-like x -defined BOOLEAN -valued Function-like V21(x) quasi_total boolean-valued Element of bool [:x,BOOLEAN:]
D is Element of x
(x,(x,y,z),C) . D is ext-real V10() V43() V44() boolean set
(x,y,(x,z,C)) . D is ext-real V10() V43() V44() boolean set
(x,(x,y,z),C) . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(x,y,z) . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
C . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
((x,y,z) . D) 'or' (C . D) is ext-real V10() V43() V44() boolean set
'not' ((x,y,z) . D) is ext-real V10() V43() V44() boolean set
K134(1,((x,y,z) . D)) is set
'not' (C . D) is ext-real V10() V43() V44() boolean set
K134(1,(C . D)) is set
('not' ((x,y,z) . D)) '&' ('not' (C . D)) is ext-real V10() V43() V44() boolean set
K131(('not' ((x,y,z) . D)),('not' (C . D))) is ext-real V10() V44() set
'not' (('not' ((x,y,z) . D)) '&' ('not' (C . D))) is ext-real V10() V43() V44() boolean set
K134(1,(('not' ((x,y,z) . D)) '&' ('not' (C . D)))) is set
y . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
z . D is ext-real V10() V43() V44() boolean Element of BOOLEAN
(y . D) 'or' (z . D) is ext-real V10() V43() V44() boolean set
'not' (y . D) is ext-real V10() V43() V44() boolean set
K134(1,(y . D)) is set
'not' (z . D) is ext-real V10() V43() V44() boolean set
K134(1,(z . D)) is set
('not' (y . D)) '&' ('not' (z . D)) is ext-real V10() V43() V44()