Logiweb codex of kvanti in pyk

Up Help

ref-2-id-99	exist {MissingArg} indeed {MissingArg}
ref-2-id-102	{MissingArg} imply {MissingArg}
ref-0-id-0	kvanti
ref-0-id-1	lemma uniqueMember
ref-0-id-2	lemma uniqueMember(Type)
ref-0-id-3	lemma sameSeries
ref-0-id-4	lemma a4
ref-0-id-5	lemma sameMember
ref-0-id-6	1rule Qclosed(Addition)
ref-0-id-7	1rule Qclosed(Multiplication)
ref-0-id-8	1rule fromCartProd(1)
ref-0-id-9	1rule fromCartProd(2)
ref-0-id-10	constantRationalSeries( {MissingArg} )
ref-0-id-11	cartProd( {MissingArg} , {MissingArg} )
ref-0-id-12	P( {MissingArg} )
ref-0-id-13	binaryUnion( {MissingArg} , {MissingArg} )
ref-0-id-14	setOfRationalSeries
ref-0-id-15	isSubset( {MissingArg} , {MissingArg} )
ref-0-id-16	(p {MissingArg} , {MissingArg} )
ref-0-id-17	(s {MissingArg} )
ref-0-id-18	cdots
ref-0-id-19	object-var
ref-0-id-20	ex-var
ref-0-id-21	ph-var
ref-0-id-22	vaerdi
ref-0-id-23	variabel
ref-0-id-24	op {MissingArg} end op
ref-0-id-25	op2 {MissingArg} comma {MissingArg} end op2
ref-0-id-26	define-equal {MissingArg} comma {MissingArg} end equal
ref-0-id-27	contains-empty {MissingArg} end empty
ref-0-id-28	Nat( {MissingArg} )
ref-0-id-29	1deduction {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-30	1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-31	1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-32	1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-33	1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-34	1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-35	1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-36	1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-37	1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-38	1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-39	1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-40	1deduction seven {MissingArg} end 1deduction
ref-0-id-41	1deduction eight {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-42	1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-43	ex1
ref-0-id-44	ex2
ref-0-id-45	ex3
ref-0-id-46	ex10
ref-0-id-47	ex20
ref-0-id-48	existential var {MissingArg} end var
ref-0-id-49	{MissingArg} is existential var
ref-0-id-50	exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-51	exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-52	exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-53	exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-54	ph1
ref-0-id-55	ph2
ref-0-id-56	ph3
ref-0-id-57	placeholder-var {MissingArg} end var
ref-0-id-58	{MissingArg} is placeholder-var
ref-0-id-59	ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-60	ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-61	ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-62	ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-63	meta-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-64	meta-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-65	meta-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-66	var big set
ref-0-id-67	object big set
ref-0-id-68	meta big set
ref-0-id-69	zermelo empty set
ref-0-id-70	system Q
ref-0-id-71	1rule mp
ref-0-id-72	1rule gen
ref-0-id-73	1rule repetition
ref-0-id-74	1rule ad absurdum
ref-0-id-75	1rule deduction
ref-0-id-76	1rule exist intro
ref-0-id-77	axiom extensionality
ref-0-id-78	axiom empty set
ref-0-id-79	axiom pair definition
ref-0-id-80	axiom union definition
ref-0-id-81	axiom power definition
ref-0-id-82	axiom separation definition
ref-0-id-83	prop lemma add double neg
ref-0-id-84	prop lemma remove double neg
ref-0-id-85	prop lemma and commutativity
ref-0-id-86	prop lemma auto imply
ref-0-id-87	prop lemma contrapositive
ref-0-id-88	prop lemma first conjunct
ref-0-id-89	prop lemma second conjunct
ref-0-id-90	prop lemma from contradiction
ref-0-id-91	prop lemma from disjuncts
ref-0-id-92	prop lemma iff commutativity
ref-0-id-93	prop lemma iff first
ref-0-id-94	prop lemma iff second
ref-0-id-95	prop lemma imply transitivity
ref-0-id-96	prop lemma join conjuncts
ref-0-id-97	prop lemma mp2
ref-0-id-98	prop lemma mp3
ref-0-id-99	prop lemma mp4
ref-0-id-100	prop lemma mp5
ref-0-id-101	prop lemma mt
ref-0-id-102	prop lemma negative mt
ref-0-id-103	prop lemma technicality
ref-0-id-104	prop lemma weakening
ref-0-id-105	prop lemma weaken or first
ref-0-id-106	prop lemma weaken or second
ref-0-id-107	lemma formula2pair
ref-0-id-108	lemma pair2formula
ref-0-id-109	lemma formula2union
ref-0-id-110	lemma union2formula
ref-0-id-111	lemma formula2separation
ref-0-id-112	lemma separation2formula
ref-0-id-113	lemma formula2power
ref-0-id-114	lemma subset in power set
ref-0-id-115	lemma power set is subset0
ref-0-id-116	lemma power set is subset
ref-0-id-117	lemma power set is subset0-switch
ref-0-id-118	lemma power set is subset-switch
ref-0-id-119	lemma set equality suff condition
ref-0-id-120	lemma set equality suff condition(t)0
ref-0-id-121	lemma set equality suff condition(t)
ref-0-id-122	lemma set equality skip quantifier
ref-0-id-123	lemma set equality nec condition
ref-0-id-124	lemma reflexivity0
ref-0-id-125	lemma reflexivity
ref-0-id-126	lemma symmetry0
ref-0-id-127	lemma symmetry
ref-0-id-128	lemma transitivity0
ref-0-id-129	lemma transitivity
ref-0-id-130	lemma er is reflexive
ref-0-id-131	lemma er is symmetric
ref-0-id-132	lemma er is transitive
ref-0-id-133	lemma empty set is subset
ref-0-id-134	lemma member not empty0
ref-0-id-135	lemma member not empty
ref-0-id-136	lemma unique empty set0
ref-0-id-137	lemma unique empty set
ref-0-id-138	lemma ==Reflexivity
ref-0-id-139	lemma ==Symmetry
ref-0-id-140	lemma ==Transitivity0
ref-0-id-141	lemma ==Transitivity
ref-0-id-142	lemma transfer ~is0
ref-0-id-143	lemma transfer ~is
ref-0-id-144	lemma pair subset0
ref-0-id-145	lemma pair subset1
ref-0-id-146	lemma pair subset
ref-0-id-147	lemma same pair
ref-0-id-148	lemma same singleton
ref-0-id-149	lemma union subset
ref-0-id-150	lemma same union
ref-0-id-151	lemma separation subset
ref-0-id-152	lemma same separation
ref-0-id-153	lemma same binary union
ref-0-id-154	lemma intersection subset
ref-0-id-155	lemma same intersection
ref-0-id-156	lemma auto member
ref-0-id-157	lemma eq-system not empty0
ref-0-id-158	lemma eq-system not empty
ref-0-id-159	lemma eq subset0
ref-0-id-160	lemma eq subset
ref-0-id-161	lemma equivalence nec condition0
ref-0-id-162	lemma equivalence nec condition
ref-0-id-163	lemma none-equivalence nec condition0
ref-0-id-164	lemma none-equivalence nec condition1
ref-0-id-165	lemma none-equivalence nec condition
ref-0-id-166	lemma equivalence class is subset
ref-0-id-167	lemma equivalence classes are disjoint
ref-0-id-168	lemma all disjoint
ref-0-id-169	lemma all disjoint-imply
ref-0-id-170	lemma bs subset union(bs/r)
ref-0-id-171	lemma union(bs/r) subset bs
ref-0-id-172	lemma union(bs/r) is bs
ref-0-id-173	theorem eq-system is partition
ref-0-id-174	var x1
ref-0-id-175	var x2
ref-0-id-176	var y1
ref-0-id-177	var y2
ref-0-id-178	var v1
ref-0-id-179	var v2
ref-0-id-180	var v3
ref-0-id-181	var v4
ref-0-id-182	var v2n
ref-0-id-183	var m1
ref-0-id-184	var m2
ref-0-id-185	var n1
ref-0-id-186	var n2
ref-0-id-187	var n3
ref-0-id-188	var ep
ref-0-id-189	var ep1
ref-0-id-190	var ep2
ref-0-id-191	var fep
ref-0-id-192	var fx
ref-0-id-193	var fy
ref-0-id-194	var fz
ref-0-id-195	var fu
ref-0-id-196	var fv
ref-0-id-197	var fw
ref-0-id-198	var rx
ref-0-id-199	var ry
ref-0-id-200	var rz
ref-0-id-201	var ru
ref-0-id-202	var sx
ref-0-id-203	var sx1
ref-0-id-204	var sy
ref-0-id-205	var sy1
ref-0-id-206	var sz
ref-0-id-207	var sz1
ref-0-id-208	var su
ref-0-id-209	var su1
ref-0-id-210	var fxs
ref-0-id-211	var fys
ref-0-id-212	var crs1
ref-0-id-213	var f1
ref-0-id-214	var f2
ref-0-id-215	var f3
ref-0-id-216	var f4
ref-0-id-217	var op1
ref-0-id-218	var op2
ref-0-id-219	var r1
ref-0-id-220	var s1
ref-0-id-221	var s2
ref-0-id-222	meta x1
ref-0-id-223	meta x2
ref-0-id-224	meta y1
ref-0-id-225	meta y2
ref-0-id-226	meta v1
ref-0-id-227	meta v2
ref-0-id-228	meta v3
ref-0-id-229	meta v4
ref-0-id-230	meta v2n
ref-0-id-231	meta m1
ref-0-id-232	meta m2
ref-0-id-233	meta n1
ref-0-id-234	meta n2
ref-0-id-235	meta n3
ref-0-id-236	meta ep
ref-0-id-237	meta ep1
ref-0-id-238	meta ep2
ref-0-id-239	meta fx
ref-0-id-240	meta fy
ref-0-id-241	meta fz
ref-0-id-242	meta fu
ref-0-id-243	meta fv
ref-0-id-244	meta fw
ref-0-id-245	meta fep
ref-0-id-246	meta rx
ref-0-id-247	meta ry
ref-0-id-248	meta rz
ref-0-id-249	meta ru
ref-0-id-250	meta sx
ref-0-id-251	meta sx1
ref-0-id-252	meta sy
ref-0-id-253	meta sy1
ref-0-id-254	meta sz
ref-0-id-255	meta sz1
ref-0-id-256	meta su
ref-0-id-257	meta su1
ref-0-id-258	meta fxs
ref-0-id-259	meta fys
ref-0-id-260	meta f1
ref-0-id-261	meta f2
ref-0-id-262	meta f3
ref-0-id-263	meta f4
ref-0-id-264	meta op1
ref-0-id-265	meta op2
ref-0-id-266	meta r1
ref-0-id-267	meta s1
ref-0-id-268	meta s2
ref-0-id-269	object ep
ref-0-id-270	object crs1
ref-0-id-271	object f1
ref-0-id-272	object f2
ref-0-id-273	object f3
ref-0-id-274	object f4
ref-0-id-275	object n1
ref-0-id-276	object n2
ref-0-id-277	object op1
ref-0-id-278	object op2
ref-0-id-279	object r1
ref-0-id-280	object s1
ref-0-id-281	object s2
ref-0-id-282	ph4
ref-0-id-283	ph5
ref-0-id-284	ph6
ref-0-id-285	NAT
ref-0-id-286	RATIONAL_SERIES
ref-0-id-287	SERIES
ref-0-id-288	setOfReals
ref-0-id-289	setOfFxs
ref-0-id-290	N
ref-0-id-291	Q
ref-0-id-292	X
ref-0-id-293	xs
ref-0-id-294	xsF
ref-0-id-295	ysF
ref-0-id-296	us
ref-0-id-297	usF
ref-0-id-298	0
ref-0-id-299	1
ref-0-id-300	(-1)
ref-0-id-301	2
ref-0-id-302	3
ref-0-id-303	1/2
ref-0-id-304	1/3
ref-0-id-305	2/3
ref-0-id-306	0f
ref-0-id-307	1f
ref-0-id-308	00
ref-0-id-309	01
ref-0-id-310	(--01)
ref-0-id-311	02
ref-0-id-312	01//02
ref-0-id-313	lemma plusAssociativity(R)
ref-0-id-314	lemma plusAssociativity(R)XX
ref-0-id-315	lemma plus0(R)
ref-0-id-316	lemma negative(R)
ref-0-id-317	lemma times1(R)
ref-0-id-318	lemma lessAddition(R)
ref-0-id-319	lemma plusCommutativity(R)
ref-0-id-320	lemma leqAntisymmetry(R)
ref-0-id-321	lemma leqTransitivity(R)
ref-0-id-322	lemma leqAddition(R)
ref-0-id-323	lemma distribution(R)
ref-0-id-324	axiom a4
ref-0-id-325	axiom induction
ref-0-id-326	axiom equality
ref-0-id-327	axiom eqLeq
ref-0-id-328	axiom eqAddition
ref-0-id-329	axiom eqMultiplication
ref-0-id-330	axiom QisClosed(reciprocal)
ref-0-id-331	lemma QisClosed(reciprocal)
ref-0-id-332	axiom QisClosed(negative)
ref-0-id-333	lemma QisClosed(negative)
ref-0-id-334	axiom leqReflexivity
ref-0-id-335	axiom leqAntisymmetry
ref-0-id-336	axiom leqTransitivity
ref-0-id-337	axiom leqTotality
ref-0-id-338	axiom leqAddition
ref-0-id-339	axiom leqMultiplication
ref-0-id-340	axiom plusAssociativity
ref-0-id-341	axiom plusCommutativity
ref-0-id-342	axiom negative
ref-0-id-343	axiom plus0
ref-0-id-344	axiom timesAssociativity
ref-0-id-345	axiom timesCommutativity
ref-0-id-346	axiom reciprocal
ref-0-id-347	axiom times1
ref-0-id-348	axiom distribution
ref-0-id-349	axiom 0not1
ref-0-id-350	lemma eqLeq(R)
ref-0-id-351	lemma timesAssociativity(R)
ref-0-id-352	lemma timesCommutativity(R)
ref-0-id-353	1rule adhoc sameR
ref-0-id-354	lemma separation2formula(1)
ref-0-id-355	lemma separation2formula(2)
ref-0-id-356	axiom cauchy
ref-0-id-357	axiom plusF
ref-0-id-358	axiom reciprocalF
ref-0-id-359	1rule from==
ref-0-id-360	1rule to==
ref-0-id-361	1rule fromInR
ref-0-id-362	lemma plusR(Sym)
ref-0-id-363	axiom reciprocalR
ref-0-id-364	1rule lessMinus1(N)
ref-0-id-365	axiom nonnegative(N)
ref-0-id-366	axiom US0
ref-0-id-367	1rule nextXS(upperBound)
ref-0-id-368	1rule nextXS(noUpperBound)
ref-0-id-369	1rule nextUS(upperBound)
ref-0-id-370	1rule nextUS(noUpperBound)
ref-0-id-371	1rule expZero
ref-0-id-372	1rule expPositive
ref-0-id-373	1rule expZero(R)
ref-0-id-374	1rule expPositive(R)
ref-0-id-375	1rule base(1/2)Sum zero
ref-0-id-376	1rule base(1/2)Sum positive
ref-0-id-377	1rule UStelescope zero
ref-0-id-378	1rule UStelescope positive
ref-0-id-379	1rule adhoc eqAddition(R)
ref-0-id-380	1rule fromLimit
ref-0-id-381	1rule toUpperBound
ref-0-id-382	1rule fromUpperBound
ref-0-id-383	axiom USisUpperBound
ref-0-id-384	axiom 0not1(R)
ref-0-id-385	1rule expUnbounded
ref-0-id-386	1rule fromLeq(Advanced)(N)
ref-0-id-387	1rule fromLeastUpperBound
ref-0-id-388	1rule toLeastUpperBound
ref-0-id-389	axiom XSisNotUpperBound
ref-0-id-390	axiom ysFGreater
ref-0-id-391	axiom ysFLess
ref-0-id-392	1rule smallInverse
ref-0-id-393	axiom natType
ref-0-id-394	axiom rationalType
ref-0-id-395	axiom seriesType
ref-0-id-396	axiom max
ref-0-id-397	axiom numerical
ref-0-id-398	axiom numericalF
ref-0-id-399	axiom memberOfSeries
ref-0-id-400	prop lemma doubly conditioned join conjuncts
ref-0-id-401	prop lemma imply negation
ref-0-id-402	prop lemma tertium non datur
ref-0-id-403	prop lemma from negated imply
ref-0-id-404	prop lemma to negated imply
ref-0-id-405	prop lemma from negated double imply
ref-0-id-406	prop lemma from negated and
ref-0-id-407	prop lemma from negated or
ref-0-id-408	prop lemma to negated or
ref-0-id-409	prop lemma from negations
ref-0-id-410	prop lemma from three disjuncts
ref-0-id-411	prop lemma from two times two disjuncts
ref-0-id-412	prop lemma negate first disjunct
ref-0-id-413	prop lemma negate second disjunct
ref-0-id-414	prop lemma expand disjuncts
ref-0-id-415	lemma set equality nec condition(1)
ref-0-id-416	lemma set equality nec condition(2)
ref-0-id-417	lemma lessLeq(R)
ref-0-id-418	lemma memberOfSeries
ref-0-id-419	lemma memberOfSeries(Type)
ref-0-id-420	{MissingArg} ^ {MissingArg}
ref-0-id-421	R( {MissingArg} )
ref-0-id-422	--R( {MissingArg} )
ref-0-id-423	1/ {MissingArg}
ref-0-id-424	eq-system of {MissingArg} modulo {MissingArg}
ref-0-id-425	intersection {MissingArg} comma {MissingArg} end intersection
ref-0-id-426	[ {MissingArg} ; {MissingArg} ]
ref-0-id-427	union {MissingArg} end union
ref-0-id-428	binary-union {MissingArg} comma {MissingArg} end union
ref-0-id-429	power {MissingArg} end power
ref-0-id-430	zermelo singleton {MissingArg} end singleton
ref-0-id-431	stateExpand( {MissingArg} , {MissingArg} , {MissingArg} )
ref-0-id-432	extractSeries( {MissingArg} )
ref-0-id-433	setOfSeries( {MissingArg} )
ref-0-id-434	--Macro( {MissingArg} )
ref-0-id-435	expandList( {MissingArg} , {MissingArg} , {MissingArg} )
ref-0-id-436	**Macro( {MissingArg} )
ref-0-id-437	++Macro( {MissingArg} )
ref-0-id-438	<
ref-0-id-439	||Macro( {MissingArg} )
ref-0-id-440	01//Macro( {MissingArg} )
ref-0-id-441	upperBound( {MissingArg} , {MissingArg} )
ref-0-id-442	leastUpperBound( {MissingArg} , {MissingArg} )
ref-0-id-443	base(1/2)Sum( {MissingArg} , {MissingArg} )
ref-0-id-444	UStelescope( {MissingArg} , {MissingArg} )
ref-0-id-445	( {MissingArg} )
ref-0-id-446	|f {MissingArg} |
ref-0-id-447	|r {MissingArg} |
ref-0-id-448	limit( {MissingArg} , {MissingArg} )
ref-0-id-449	U( {MissingArg} )
ref-0-id-450	isOrderedPair( {MissingArg} , {MissingArg} , {MissingArg} )
ref-0-id-451	isRelation( {MissingArg} , {MissingArg} , {MissingArg} )
ref-0-id-452	isFunction( {MissingArg} , {MissingArg} , {MissingArg} )
ref-0-id-453	isSeries( {MissingArg} , {MissingArg} )
ref-0-id-454	isNatural( {MissingArg} )
ref-0-id-455	(o {MissingArg} , {MissingArg} )
ref-0-id-456	typeNat( {MissingArg} )
ref-0-id-457	typeNat0( {MissingArg} )
ref-0-id-458	typeRational( {MissingArg} )
ref-0-id-459	typeRational0( {MissingArg} )
ref-0-id-460	typeSeries( {MissingArg} , {MissingArg} )
ref-0-id-461	typeSeries0( {MissingArg} , {MissingArg} )
ref-0-id-462	zermelo pair {MissingArg} comma {MissingArg} end pair
ref-0-id-463	zermelo ordered pair {MissingArg} comma {MissingArg} end pair
ref-0-id-464	- {MissingArg}
ref-0-id-465	-f {MissingArg}
ref-0-id-466	-- {MissingArg}
ref-0-id-467	1f/ {MissingArg}
ref-0-id-468	01// {MissingArg}
ref-0-id-469	{MissingArg} is related to {MissingArg} under {MissingArg}
ref-0-id-470	{MissingArg} is reflexive relation in {MissingArg}
ref-0-id-471	{MissingArg} is symmetric relation in {MissingArg}
ref-0-id-472	{MissingArg} is transitive relation in {MissingArg}
ref-0-id-473	{MissingArg} is equivalence relation in {MissingArg}
ref-0-id-474	equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
ref-0-id-475	{MissingArg} is partition of {MissingArg}
ref-0-id-476	{MissingArg} * {MissingArg}
ref-0-id-477	{MissingArg} *f {MissingArg}
ref-0-id-478	{MissingArg} ** {MissingArg}
ref-0-id-479	{MissingArg} + {MissingArg}
ref-0-id-480	{MissingArg} - {MissingArg}
ref-0-id-481	{MissingArg} +f {MissingArg}
ref-0-id-482	{MissingArg} -f {MissingArg}
ref-0-id-483	{MissingArg} ++ {MissingArg}
ref-0-id-484	R( {MissingArg} ) -- R( {MissingArg} )
ref-0-id-485	{MissingArg} in0 {MissingArg}
ref-0-id-486	| {MissingArg} |
ref-0-id-487	if( {MissingArg} , {MissingArg} , {MissingArg} )
ref-0-id-488	max( {MissingArg} , {MissingArg} )
ref-0-id-489	maxR( {MissingArg} , {MissingArg} )
ref-0-id-490	{MissingArg} = {MissingArg}
ref-0-id-491	{MissingArg} != {MissingArg}
ref-0-id-492	{MissingArg} <= {MissingArg}
ref-0-id-493	{MissingArg} < {MissingArg}
ref-0-id-494	{MissingArg}
ref-0-id-495	{MissingArg} <=f {MissingArg}
ref-0-id-496	{MissingArg} sameF {MissingArg}
ref-0-id-497	{MissingArg} == {MissingArg}
ref-0-id-498	{MissingArg} !!== {MissingArg}
ref-0-id-499	{MissingArg} << {MissingArg}
ref-0-id-500	{MissingArg} <<== {MissingArg}
ref-0-id-501	{MissingArg} zermelo is {MissingArg}
ref-0-id-502	{MissingArg} is subset of {MissingArg}
ref-0-id-503	not0 {MissingArg}
ref-0-id-504	{MissingArg} zermelo ~in {MissingArg}
ref-0-id-505	{MissingArg} zermelo ~is {MissingArg}
ref-0-id-506	{MissingArg} and0 {MissingArg}
ref-0-id-507	{MissingArg} or0 {MissingArg}
ref-0-id-508	exist0 {MissingArg} indeed {MissingArg}
ref-0-id-509	{MissingArg} iff {MissingArg}
ref-0-id-510	the set of ph in {MissingArg} such that {MissingArg} end set