include('Axioms/gcdset_2.ax').
tff(tp_c_2Eset__relation_2ERREFL__EXP,type,(c_2Eset__relation_2ERREFL__EXP:del > $i)).
tff(mem_c_2Eset__relation_2ERREFL__EXP,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2ERREFL__EXP(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(arr(A_27a,bool),arr(A_27a,arr(A_27a,bool))))))).
tff(tp_c_2Eset__relation_2ERRUNIV,type,(c_2Eset__relation_2ERRUNIV:del > $i)).
tff(mem_c_2Eset__relation_2ERRUNIV,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2ERRUNIV(A_27a),arr(arr(A_27a,bool),arr(A_27a,arr(A_27a,bool)))))).
tff(tp_c_2Eset__relation_2Eacyclic,type,(c_2Eset__relation_2Eacyclic:del > $i)).
tff(mem_c_2Eset__relation_2Eacyclic,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eacyclic(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)))).
tff(tp_c_2Eset__relation_2Eall__choices,type,(c_2Eset__relation_2Eall__choices:del > $i)).
tff(mem_c_2Eset__relation_2Eall__choices,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eall__choices(A_27a),arr(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Eset__relation_2Eantisym,type,(c_2Eset__relation_2Eantisym:del > $i)).
tff(mem_c_2Eset__relation_2Eantisym,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eantisym(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)))).
tff(tp_c_2Eset__relation_2Echain,type,(c_2Eset__relation_2Echain:del > $i)).
tff(mem_c_2Eset__relation_2Echain,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Echain(A_27a),arr(arr(A_27a,bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool))))).
tff(tp_c_2Eset__relation_2Edomain,type,(c_2Eset__relation_2Edomain:(del * del) > $i)).
tff(mem_c_2Eset__relation_2Edomain,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eset__relation_2Edomain(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),arr(A_27a,bool)))))).
tff(tp_c_2Eset__relation_2Efchains,type,(c_2Eset__relation_2Efchains:del > $i)).
tff(mem_c_2Eset__relation_2Efchains,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Efchains(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Eset__relation_2Efinite__prefixes,type,(c_2Eset__relation_2Efinite__prefixes:(del * del) > $i)).
tff(mem_c_2Eset__relation_2Efinite__prefixes,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),arr(arr(A_27b,bool),bool)))))).
tff(tp_c_2Eset__relation_2Eget__min,type,(c_2Eset__relation_2Eget__min:del > $i)).
tff(mem_c_2Eset__relation_2Eget__min,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eget__min(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),ty_2Eoption_2Eoption(A_27a)))))).
tff(tp_c_2Eset__relation_2Eirreflexive,type,(c_2Eset__relation_2Eirreflexive:del > $i)).
tff(mem_c_2Eset__relation_2Eirreflexive,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eirreflexive(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Eset__relation_2Elinear__order,type,(c_2Eset__relation_2Elinear__order:del > $i)).
tff(mem_c_2Eset__relation_2Elinear__order,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Elinear__order(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Eset__relation_2Emaximal__elements,type,(c_2Eset__relation_2Emaximal__elements:del > $i)).
tff(mem_c_2Eset__relation_2Emaximal__elements,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Emaximal__elements(A_27a),arr(arr(A_27a,bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(A_27a,bool)))))).
tff(tp_c_2Eset__relation_2Eminimal__elements,type,(c_2Eset__relation_2Eminimal__elements:del > $i)).
tff(mem_c_2Eset__relation_2Eminimal__elements,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eminimal__elements(A_27a),arr(arr(A_27a,bool),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(A_27a,bool)))))).
tff(tp_c_2Eset__relation_2Enth__min,type,(c_2Eset__relation_2Enth__min:del > $i)).
tff(mem_c_2Eset__relation_2Enth__min,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Enth__min(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),arr(ty_2Enum_2Enum,ty_2Eoption_2Eoption(A_27a))))))).
tff(tp_c_2Eset__relation_2Enum__order,type,(c_2Eset__relation_2Enum__order:del > $i)).
tff(mem_c_2Eset__relation_2Enum__order,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Enum__order(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)))))).
tff(tp_c_2Eset__relation_2Epartial__order,type,(c_2Eset__relation_2Epartial__order:del > $i)).
tff(mem_c_2Eset__relation_2Epartial__order,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Epartial__order(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Eset__relation_2Eper,type,(c_2Eset__relation_2Eper:del > $i)).
tff(mem_c_2Eset__relation_2Eper,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eper(A_27a),arr(arr(A_27a,bool),arr(arr(arr(A_27a,bool),bool),bool))))).
tff(tp_c_2Eset__relation_2Eper__restrict,type,(c_2Eset__relation_2Eper__restrict:del > $i)).
tff(mem_c_2Eset__relation_2Eper__restrict,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Eper__restrict(A_27a),arr(arr(arr(A_27a,bool),bool),arr(arr(A_27a,bool),arr(arr(A_27a,bool),bool)))))).
tff(tp_c_2Eset__relation_2Erange,type,(c_2Eset__relation_2Erange:(del * del) > $i)).
tff(mem_c_2Eset__relation_2Erange,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eset__relation_2Erange(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27b,A_27a),bool),arr(A_27a,bool)))))).
tff(tp_c_2Eset__relation_2Ercomp,type,(c_2Eset__relation_2Ercomp:(del * del * del) > $i)).
tff(mem_c_2Eset__relation_2Ercomp,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),arr(arr(ty_2Epair_2Eprod(A_27a,A_27c),bool),arr(arr(ty_2Epair_2Eprod(A_27c,A_27b),bool),arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)))))))).
tff(tp_c_2Eset__relation_2Ereflexive,type,(c_2Eset__relation_2Ereflexive:del > $i)).
tff(mem_c_2Eset__relation_2Ereflexive,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Ereflexive(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Eset__relation_2Erel__to__reln,type,(c_2Eset__relation_2Erel__to__reln:(del * del) > $i)).
tff(mem_c_2Eset__relation_2Erel__to__reln,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,bool)),arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)))))).
tff(tp_c_2Eset__relation_2Ereln__to__rel,type,(c_2Eset__relation_2Ereln__to__rel:(del * del) > $i)).
tff(mem_c_2Eset__relation_2Ereln__to__rel,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),arr(arr(ty_2Epair_2Eprod(A_27a,A_27b),bool),arr(A_27a,arr(A_27b,bool))))))).
tff(tp_c_2Eset__relation_2Errestrict,type,(c_2Eset__relation_2Errestrict:del > $i)).
tff(mem_c_2Eset__relation_2Errestrict,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Errestrict(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)))))).
tff(tp_c_2Eset__relation_2Estrict,type,(c_2Eset__relation_2Estrict:del > $i)).
tff(mem_c_2Eset__relation_2Estrict,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Estrict(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))))).
tff(tp_c_2Eset__relation_2Estrict__linear__order,type,(c_2Eset__relation_2Estrict__linear__order:del > $i)).
tff(mem_c_2Eset__relation_2Estrict__linear__order,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Estrict__linear__order(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Eset__relation_2Etc,type,(c_2Eset__relation_2Etc:del > $i)).
tff(mem_c_2Eset__relation_2Etc,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Etc(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))))).
tff(tp_c_2Eset__relation_2Etransitive,type,(c_2Eset__relation_2Etransitive:del > $i)).
tff(mem_c_2Eset__relation_2Etransitive,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Etransitive(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)))).
tff(tp_c_2Eset__relation_2Euniv__reln,type,(c_2Eset__relation_2Euniv__reln:del > $i)).
tff(mem_c_2Eset__relation_2Euniv__reln,axiom,( ! [A_27a:del] : mem(c_2Eset__relation_2Euniv__reln(A_27a),arr(arr(A_27a,bool),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))))).
tff(tp_c_2Eset__relation_2Eupper__bounds,type,(c_2Eset__relation_2Eupper__bounds:(del * del) > $i)).
tff(mem_c_2Eset__relation_2Eupper__bounds,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eset__relation_2Eupper__bounds(A_27a,A_27b),arr(arr(A_27b,bool),arr(arr(ty_2Epair_2Eprod(A_27b,A_27a),bool),arr(A_27a,bool))))))).
tff(conj_thm_2Eset__relation_2Erextension,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1t:$i] : (mem(V1t,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ((V0s = V1t) <=> ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27b) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),V0s)) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x),V3y)),V1t)))))))))))))))).
tff(ax_thm_2Eset__relation_2Edomain__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V0r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f318(A_27b,A_27a,V0r)))))))).
tff(ax_thm_2Eset__relation_2Erange__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => (ap(c_2Eset__relation_2Erange(A_27a,A_27b),V0r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f320(A_27b,A_27a,V0r)))))))).
tff(conj_thm_2Eset__relation_2Ein__domain,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V1r))) <=> (? [V2y:$i] : (mem(V2y,A_27b) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V2y)),V1r))))))))))))).
tff(conj_thm_2Eset__relation_2Ein__range,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0y:$i] : (mem(V0y,A_27a) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0y),ap(c_2Eset__relation_2Erange(A_27a,A_27b),V1r))) <=> (? [V2x:$i] : (mem(V2x,A_27b) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27a)),ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V2x),V0y)),V1r))))))))))))).
tff(conj_thm_2Eset__relation_2Ein__dom__rg,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27b) => ( ! [V2r:$i] : (mem(V2r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y)),V2r)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V2r))) & p(ap(ap(c_2Ebool_2EIN(A_27b),V1y),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V2r))))))))))))))).
tff(conj_thm_2Eset__relation_2Edomain__mono,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1r_27:$i] : (mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V0r),V1r_27)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V0r)),ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V1r_27)))))))))))).
tff(conj_thm_2Eset__relation_2Erange__mono,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1r_27:$i] : (mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V0r),V1r_27)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V1r_27)))))))))))).
tff(ax_thm_2Eset__relation_2Errestrict__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f322(A_27a,V1s,V0r)))))))))).
tff(conj_thm_2Eset__relation_2Ein__rrestrict,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ( ! [V2r:$i] : (mem(V2r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V2r),V3s))) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),V2r)) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),V3s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V1y),V3s)))))))))))))))).
tff(conj_thm_2Eset__relation_2Ein__rrestrict__alt,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Epair_2Eprod(A_27a,A_27a)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),V0x),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r),V2s))) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),V0x),V1r)) & (p(ap(ap(c_2Ebool_2EIN(A_27a),ap(c_2Epair_2EFST(A_27a,A_27a),V0x)),V2s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),ap(c_2Epair_2ESND(A_27a,A_27a),V0x)),V2s)))))))))))))).
tff(conj_thm_2Eset__relation_2Errestrict__SUBSET,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s)),V0r))))))))).
tff(conj_thm_2Eset__relation_2Errestrict__union,lemma,(( ! [A_27a:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0r1),V1r2)),V2s) = ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r1),V2s)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r2),V2s)))))))))))).
tff(conj_thm_2Eset__relation_2Errestrict__rrestrict,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,arr(A_27a,bool)) => ( ! [V2y:$i] : (mem(V2y,arr(A_27a,bool)) => (ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1x)),V2y) = ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),ap(ap(c_2Epred__set_2EINTER(A_27a),V1x),V2y)))))))))))).
tff(conj_thm_2Eset__relation_2Edomain__rrestrict__SUBSET,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))),V1s))))))))).
tff(conj_thm_2Eset__relation_2Erange__rrestrict__SUBSET,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))),V1s))))))))).
tff(ax_thm_2Eset__relation_2Ercomp__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27c),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27c,A_27b),bool)) => (ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),V0r1),V1r2) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),bool)),f325(A_27c,A_27a,A_27b,V0r1,V1r2)))))))))))).
tff(ax_thm_2Eset__relation_2Estrict__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(c_2Eset__relation_2Estrict(A_27a),V0r) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f327(A_27a,V0r)))))))).
tff(conj_thm_2Eset__relation_2Estrict__rrestrict,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (ap(c_2Eset__relation_2Estrict(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s)) = ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r)),V1s))))))))).
tff(ax_thm_2Eset__relation_2Euniv__reln__def,axiom,( ! [A_27a:del]: ( ! [V0xs:$i] : (mem(V0xs,arr(A_27a,bool)) => (ap(c_2Eset__relation_2Euniv__reln(A_27a),V0xs) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f329(A_27a,V0xs)))))))).
tff(ax_thm_2Eset__relation_2Efinite__prefixes__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => (p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) <=> ( ! [V2e:$i] : (mem(V2e,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V2e),V1s)) => p(ap(c_2Epred__set_2EFINITE(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f330(A_27b,A_27a,V0r,V2e))))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__subset__s,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => ( ! [V2s_27:$i] : (mem(V2s_27,arr(A_27b,bool)) => ((p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),V2s_27),V1s))) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V2s_27))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__subset__r,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1r_27:$i] : (mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => ((p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V2s)) & p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V1r_27),V0r))) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V1r_27),V2s))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__subset__rs,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => ( ! [V2r_27:$i] : (mem(V2r_27,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V3s_27:$i] : (mem(V3s_27,arr(A_27b,bool)) => (p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) => (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27b)),V2r_27),V0r)) => (p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),V3s_27),V1s)) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V2r_27),V3s_27))))))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__subset,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2s_27:$i] : (mem(V2s_27,arr(A_27a,bool)) => ((p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2s_27),V1s))) => (p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),V0r),V2s_27)) & p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V2s_27)),V2s_27))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__union,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V2s1:$i] : (mem(V2s1,arr(A_27b,bool)) => ( ! [V3s2:$i] : (mem(V3s2,arr(A_27b,bool)) => ((p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r1),V2s1)) & p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V1r2),V3s2))) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27b)),V0r1),V1r2)),ap(ap(c_2Epred__set_2EINTER(A_27b),V2s1),V3s2)))))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__comp,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27b,A_27c),bool)) => ( ! [V2s1:$i] : (mem(V2s1,arr(A_27b,bool)) => ( ! [V3s2:$i] : (mem(V3s2,arr(A_27c,bool)) => ((p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r1),V2s1)) & (p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27b,A_27c),V1r2),V3s2)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),ap(c_2Epred__set_2EGSPEC(A_27b,A_27b),f332(A_27c,A_27b,V1r2,V3s2))),V2s1)))) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27c),ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27c,A_27b),V0r1),V1r2)),V3s2)))))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__inj__image,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ((( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((ap(V0f,V3x) = ap(V0f,V4y)) => (V3x = V4y)))))) & p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27a),V1r),V2s))) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27b,A_27b),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27b,A_27b),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27b,A_27b),bool)),f334(A_27b,A_27a,V0f,V1r)))),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),V2s)))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__prefixes__range,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27b,bool)) => ((p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),V1s)) & p(ap(ap(c_2Epred__set_2EDISJOINT(A_27b),V2t),ap(c_2Eset__relation_2Erange(A_27b,A_27a),V0r)))) => p(ap(ap(c_2Eset__relation_2Efinite__prefixes(A_27a,A_27b),V0r),ap(ap(c_2Epred__set_2EUNION(A_27b),V1s),V2t)))))))))))))).
tff(ax_thm_2Eset__relation_2Etc__def,axiom,( ! [A_27a:del]: (c_2Eset__relation_2Etc(A_27a) = f343(A_27a)))).
tff(conj_thm_2Eset__relation_2Etc__rules,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r)))))))) & ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((? [V5z:$i] : (mem(V5z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3x),V5z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V5z),V4y)),ap(c_2Eset__relation_2Etc(A_27a),V0r)))))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3x),V4y)),ap(c_2Eset__relation_2Etc(A_27a),V0r)))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__cases,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) | (? [V3z:$i] : (mem(V3z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3z),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__ind,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1tc_27:$i] : (mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((? [V6z:$i] : (mem(V6z,A_27a) & (p(ap(ap(V1tc_27,V4x),V6z)) & p(ap(ap(V1tc_27,V6z),V5y))))) => p(ap(ap(V1tc_27,V4x),V5y)))))))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__closure,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),ap(c_2Eset__relation_2Etc(A_27a),V1s))) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Eset__relation_2Etc(A_27a),V0r)),ap(c_2Eset__relation_2Etc(A_27a),V1s))))))))))).
tff(conj_thm_2Eset__relation_2Esubset__tc,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),ap(c_2Eset__relation_2Etc(A_27a),V0r)))))))).
tff(conj_thm_2Eset__relation_2Etc__idemp,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(c_2Eset__relation_2Etc(A_27a),ap(c_2Eset__relation_2Etc(A_27a),V0r)) = ap(c_2Eset__relation_2Etc(A_27a),V0r))))))).
tff(conj_thm_2Eset__relation_2Etc__mono,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),V1s)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Eset__relation_2Etc(A_27a),V0r)),ap(c_2Eset__relation_2Etc(A_27a),V1s))))))))))).
tff(conj_thm_2Eset__relation_2Etc__strongind,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1tc_27:$i] : (mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((? [V6z:$i] : (mem(V6z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & (p(ap(ap(V1tc_27,V4x),V6z)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(V1tc_27,V6z),V5y))))))) => p(ap(ap(V1tc_27,V4x),V5y)))))))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__cases__right,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) | (? [V3z:$i] : (mem(V3z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3z),V2y)),V0r)))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__cases__left,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) | (? [V3z:$i] : (mem(V3z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),V0r)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3z),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__ind__left,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1tc_27:$i] : (mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((? [V6z:$i] : (mem(V6z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),V0r)) & p(ap(ap(V1tc_27,V6z),V5y))))) => p(ap(ap(V1tc_27,V4x),V5y)))))))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__strongind__left,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1tc_27:$i] : (mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((? [V6z:$i] : (mem(V6z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),V0r)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & p(ap(ap(V1tc_27,V6z),V5y)))))) => p(ap(ap(V1tc_27,V4x),V5y)))))))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__ind__right,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1tc_27:$i] : (mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((? [V6z:$i] : (mem(V6z,A_27a) & (p(ap(ap(V1tc_27,V4x),V6z)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),V0r))))) => p(ap(ap(V1tc_27,V4x),V5y)))))))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y))))))))))))))).
tff(conj_thm_2Eset__relation_2Ertc__ind__right,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1tc_27:$i] : (mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r))) | p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)))) => p(ap(ap(V1tc_27,V2x),V2x))))) & ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((? [V5z:$i] : (mem(V5z,A_27a) & (p(ap(ap(V1tc_27,V3x),V5z)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V5z),V4y)),V0r))))) => p(ap(ap(V1tc_27,V3x),V4y)))))))) => ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7y:$i] : (mem(V7y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6x),V7y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V6x),V7y))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__strongind__right,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1tc_27:$i] : (mem(V1tc_27,arr(A_27a,arr(A_27a,bool))) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) => p(ap(ap(V1tc_27,V2x),V3y))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((? [V6z:$i] : (mem(V6z,A_27a) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V6z)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) & (p(ap(ap(V1tc_27,V4x),V6z)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6z),V5y)),V0r)))))) => p(ap(ap(V1tc_27,V4x),V5y)))))))) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ( ! [V8y:$i] : (mem(V8y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V7x),V8y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => p(ap(ap(V1tc_27,V7x),V8y))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__union,lemma,(( ! [A_27a:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r1))) => ( ! [V3r2:$i] : (mem(V3r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0r1),V3r2)))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__implication,lemma,(( ! [A_27a:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r1)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V1r2))))))) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V0r1))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V5y)),ap(c_2Eset__relation_2Etc(A_27a),V1r2)))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__empty,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => (~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Etc(A_27a),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__empty__eqn,lemma,(( ! [A_27a:del]: (ap(c_2Eset__relation_2Etc(A_27a),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a))) = c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a)))))).
tff(conj_thm_2Eset__relation_2Etc__domain__range,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2y),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)))))))))))))).
tff(conj_thm_2Eset__relation_2Errestrict__tc,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,arr(A_27a,bool)) => ( ! [V2e:$i] : (mem(V2e,A_27a) => ( ! [V3e_27:$i] : (mem(V3e_27,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2e),V3e_27)),ap(c_2Eset__relation_2Etc(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1x)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2e),V3e_27)),ap(c_2Eset__relation_2Etc(A_27a),V0r))))))))))))))).
tff(conj_thm_2Eset__relation_2Etc__SWAP,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(c_2Eset__relation_2Etc(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),V0r)) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),ap(c_2Eset__relation_2Etc(A_27a),V0r)))))))).
tff(ax_thm_2Eset__relation_2Eacyclic__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) <=> ( ! [V1x:$i] : (mem(V1x,A_27a) => (~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V1x)),ap(c_2Eset__relation_2Etc(A_27a),V0r))))))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__subset,lemma,(( ! [A_27a:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ((p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r1)) & p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V1r2),V0r1))) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r2)))))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__rrestrict,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))))))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__irreflexive,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) => (~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V1x)),V0r))))))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__SWAP,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),V0r))) <=> p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__bigunion,lemma,(( ! [A_27a:del]: ( ! [V0rs:$i] : (mem(V0rs,arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) => ((( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V2r_27:$i] : (mem(V2r_27,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),V1r),V0rs)) & (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),V2r_27),V0rs)) & (~~ (V1r = V2r_27)))) => p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r))),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V2r_27)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V2r_27))))))))) & ( ! [V3r:$i] : (mem(V3r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)),V3r),V0rs)) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),V3r)))))) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(c_2Epred__set_2EBIGUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0rs))))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__union,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1r_27:$i] : (mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ((p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r_27)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r_27)))) & (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) & p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r_27)))) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),V1r_27))))))))))).
tff(ax_thm_2Eset__relation_2Ereflexive__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),V1s)) <=> ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V2x)),V0r)))))))))))).
tff(ax_thm_2Eset__relation_2Eirreflexive__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V0r),V1s)) <=> ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) => (~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V2x)),V0r))))))))))))).
tff(ax_thm_2Eset__relation_2Etransitive__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) <=> ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2y),V3z)),V0r))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V3z)),V0r)))))))))))))).
tff(conj_thm_2Eset__relation_2Etransitive__tc,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) => (ap(c_2Eset__relation_2Etc(A_27a),V0r) = V0r))))))).
tff(conj_thm_2Eset__relation_2Etc__transitive,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(c_2Eset__relation_2Etransitive(A_27a),ap(c_2Eset__relation_2Etc(A_27a),V0r)))))))).
tff(ax_thm_2Eset__relation_2Eantisym__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) <=> ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),V0r)) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2y),V1x)),V0r))) => (V1x = V2y))))))))))).
tff(ax_thm_2Eset__relation_2Epartial__order__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) <=> (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),V1s)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)),V1s)) & (p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & (p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),V1s)) & p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r))))))))))))).
tff(conj_thm_2Eset__relation_2Eantisym__subset,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eantisym(A_27a),V0t)) => (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V1s),V0t)) => p(ap(c_2Eset__relation_2Eantisym(A_27a),V1s))))))))))).
tff(conj_thm_2Eset__relation_2Epartial__order__dom__rng,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) & p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s))))))))))))))).
tff(conj_thm_2Eset__relation_2Epartial__order__subset,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2s_27:$i] : (mem(V2s_27,arr(A_27a,bool)) => ((p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2s_27),V1s))) => p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V2s_27)),V2s_27)))))))))))).
tff(conj_thm_2Eset__relation_2Estrict__partial__order,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) => (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))),V1s)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))),V1s)) & (p(ap(c_2Eset__relation_2Etransitive(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))) & p(ap(c_2Eset__relation_2Eantisym(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r)))))))))))))).
tff(conj_thm_2Eset__relation_2Estrict__partial__order__acyclic,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) => p(ap(c_2Eset__relation_2Eacyclic(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))))))))))).
tff(ax_thm_2Eset__relation_2Elinear__order__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s)) <=> (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),V1s)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)),V1s)) & (p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & (p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) & ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V2x)),V0r))))))))))))))))))).
tff(conj_thm_2Eset__relation_2Elinear__order__subset,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2s_27:$i] : (mem(V2s_27,arr(A_27a,bool)) => ((p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2s_27),V1s))) => p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V2s_27)),V2s_27)))))))))))).
tff(conj_thm_2Eset__relation_2Epartial__order__linear__order,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s)) => p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)))))))))).
tff(ax_thm_2Eset__relation_2Estrict__linear__order__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V0r),V1s)) <=> (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),V1s)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)),V1s)) & (p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & (( ! [V2x:$i] : (mem(V2x,A_27a) => (~~ p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V2x)),V0r))))) & ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1s)) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V4y),V1s)) & (~~ (V3x = V4y)))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3x),V4y)),V0r)) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4y),V3x)),V0r))))))))))))))))))).
tff(conj_thm_2Eset__relation_2Estrict__linear__order__dom__rng,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) & p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V0r),V1s))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s))))))))))))))).
tff(conj_thm_2Eset__relation_2Elinear__order__dom__rng,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),V0r)) & p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),V1s))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s))))))))))))))).
tff(ax_thm_2Eset__relation_2Ereln__to__rel__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r) = f344(A_27b,A_27a,V0r))))))).
tff(ax_thm_2Eset__relation_2Erel__to__reln__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => (ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V0R) = ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),bool)),f346(A_27a,A_27b,V0R))))))))).
tff(ax_thm_2Eset__relation_2ERRUNIV__def,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (ap(c_2Eset__relation_2ERRUNIV(A_27a),V0s) = f348(A_27a,V0s)))))).
tff(ax_thm_2Eset__relation_2ERREFL__EXP__def,axiom,( ! [A_27a:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V0R),V1s) = ap(ap(c_2Erelation_2ERUNION(A_27a,A_27a),V0R),f350(A_27a,V1s))))))))).
tff(conj_thm_2Eset__relation_2ERREFL__EXP__RSUBSET,lemma,(( ! [A_27a:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Erelation_2ERSUBSET(A_27a,A_27a),V0R),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V0R),V1s)))))))))).
tff(conj_thm_2Eset__relation_2ERREFL__EXP__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => (ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V0R),c_2Epred__set_2EUNIV(A_27a)) = V0R)))))).
tff(conj_thm_2Eset__relation_2EREL__RESTRICT__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => (ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),V0R),c_2Epred__set_2EUNIV(A_27a)) = V0R)))))).
tff(conj_thm_2Eset__relation_2Ein__rel__to__reln,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0xy:$i] : (mem(V0xy,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V1R:$i] : (mem(V1R,arr(A_27a,arr(A_27b,bool))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),V0xy),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R))) <=> p(ap(ap(V1R,ap(c_2Epair_2EFST(A_27a,A_27b),V0xy)),ap(c_2Epair_2ESND(A_27a,A_27b),V0xy)))))))))))).
tff(conj_thm_2Eset__relation_2Ereln__to__rel__app,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27b) => (p(ap(ap(ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r),V1x),V2y)) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V1x),V2y)),V0r))))))))))))).
tff(conj_thm_2Eset__relation_2Erel__to__reln__IS__UNCURRY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (c_2Eset__relation_2Erel__to__reln(A_27a,A_27b) = c_2Epair_2EUNCURRY(A_27a,A_27b,bool)))))).
tff(conj_thm_2Eset__relation_2Ereln__to__rel__IS__CURRY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b) = c_2Epair_2ECURRY(A_27a,A_27b,bool)))))).
tff(conj_thm_2Eset__relation_2Erel__to__reln__inv,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => (ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V0R)) = V0R))))))).
tff(conj_thm_2Eset__relation_2Ereln__to__rel__inv,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r)) = V0r))))))).
tff(conj_thm_2Eset__relation_2Ereln__to__rel__11,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ((ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r1) = ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V1r2)) <=> (V0r1 = V1r2)))))))))).
tff(conj_thm_2Eset__relation_2Erel__to__reln__11,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R1:$i] : (mem(V0R1,arr(A_27a,arr(A_27b,bool))) => ( ! [V1R2:$i] : (mem(V1R2,arr(A_27a,arr(A_27b,bool))) => ((ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V0R1) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R2)) <=> (V0R1 = V1R2)))))))))).
tff(conj_thm_2Eset__relation_2Erel__to__reln__swap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V1R:$i] : (mem(V1R,arr(A_27a,arr(A_27b,bool))) => ((V0r = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R)) <=> (ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r) = V1R)))))))))).
tff(conj_thm_2Eset__relation_2Edomain__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => (ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V0r) = ap(c_2Erelation_2ERDOM(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V0r))))))))).
tff(conj_thm_2Eset__relation_2Erange__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => (ap(c_2Eset__relation_2Erange(A_27a,A_27b),V0r) = ap(c_2Erelation_2ERRANGE(A_27b,A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27b,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Estrict__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(c_2Eset__relation_2Estrict(A_27a),V0r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ESTRORD(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Errestrict__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s)))))))))).
tff(conj_thm_2Eset__relation_2Ercomp__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0r1:$i] : (mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27c),bool)) => ( ! [V1r2:$i] : (mem(V1r2,arr(ty_2Epair_2Eprod(A_27c,A_27b),bool)) => (ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),V0r1),V1r2) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(ap(c_2Erelation_2EO(A_27a,A_27c,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27c,A_27b),V1r2)),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27c),V0r1))))))))))))).
tff(conj_thm_2Eset__relation_2Euniv__reln__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (ap(c_2Eset__relation_2Euniv__reln(A_27a),V0s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Eset__relation_2ERRUNIV(A_27a),V0s)))))))).
tff(conj_thm_2Eset__relation_2Etc__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(c_2Eset__relation_2Etc(A_27a),V0r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__reln__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V0r)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)))))))))).
tff(conj_thm_2Eset__relation_2Eirreflexive__reln__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V0r),V1s)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s))))))))))).
tff(conj_thm_2Eset__relation_2Eirreflexive__reln__to__rel__conv__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Ereflexive__reln__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),V1s)) <=> p(ap(c_2Erelation_2Ereflexive(A_27a),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s))))))))))).
tff(conj_thm_2Eset__relation_2Ereflexive__reln__to__rel__conv__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2Ereflexive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Etransitive__reln__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) <=> p(ap(c_2Erelation_2Etransitive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Eantisym__reln__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) <=> p(ap(c_2Erelation_2Eantisymmetric(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Epartial__order__reln__to__rel__conv,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),V1s)) <=> (p(ap(ap(c_2Erelation_2ERSUBSET(A_27a,A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2ERRUNIV(A_27a),V1s))) & p(ap(c_2Erelation_2EWeakOrder(A_27a),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r)),V1s)))))))))))).
tff(conj_thm_2Eset__relation_2Epartial__order__reln__to__rel__conv__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Elinear__order__reln__to__rel__conv__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Estrict__linear__order__reln__to__rel__conv__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V0r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))))))))).
tff(conj_thm_2Eset__relation_2Ereln__rel__conv__thms,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0xy:$i] : (mem(V0xy,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V1R:$i] : (mem(V1R,arr(A_27a,arr(A_27b,bool))) => ( ! [V2r:$i] : (mem(V2r,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27b) => ( ! [V5r1:$i] : (mem(V5r1,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V6r2:$i] : (mem(V6r2,arr(ty_2Epair_2Eprod(A_27a,A_27b),bool)) => ( ! [V7R1:$i] : (mem(V7R1,arr(A_27a,arr(A_27b,bool))) => ( ! [V8R2:$i] : (mem(V8R2,arr(A_27a,arr(A_27b,bool))) => ( ! [V9R:$i] : (mem(V9R,arr(A_27a,arr(A_27a,bool))) => ( ! [V10r:$i] : (mem(V10r,arr(ty_2Epair_2Eprod(A_27b,A_27a),bool)) => ( ! [V11r:$i] : (mem(V11r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V12s:$i] : (mem(V12s,arr(A_27a,bool)) => ( ! [V13r1:$i] : (mem(V13r1,arr(ty_2Epair_2Eprod(A_27a,A_27c),bool)) => ( ! [V14r2:$i] : (mem(V14r2,arr(ty_2Epair_2Eprod(A_27c,A_27b),bool)) => (((p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),V0xy),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R))) <=> p(ap(ap(V1R,ap(c_2Epair_2EFST(A_27a,A_27b),V0xy)),ap(c_2Epair_2ESND(A_27a,A_27b),V0xy)))) & ((p(ap(ap(ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V2r),V3x),V4y)) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V3x),V4y)),V2r))) & ((ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V1R)) = V1R) & ((ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V2r)) = V2r) & (((ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V5r1) = ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V6r2)) <=> (V5r1 = V6r2)) & ((ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V7R1) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),V8R2)) <=> (V7R1 = V8R2))))))) & ((ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),V9R),c_2Epred__set_2EUNIV(A_27a)) = V9R) & ((ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),V9R),c_2Epred__set_2EUNIV(A_27a)) = V9R) & ((ap(c_2Eset__relation_2Edomain(A_27a,A_27b),V2r) = ap(c_2Erelation_2ERDOM(A_27a,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27b),V2r))) & ((ap(c_2Eset__relation_2Erange(A_27a,A_27b),V10r) = ap(c_2Erelation_2ERRANGE(A_27b,A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27b,A_27a),V10r))) & ((ap(c_2Eset__relation_2Estrict(A_27a),V11r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ESTRORD(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))) & ((ap(ap(c_2Eset__relation_2Errestrict(A_27a),V11r),V12s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)),V12s))) & ((ap(ap(c_2Eset__relation_2Ercomp(A_27a,A_27b,A_27c),V13r1),V14r2) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27b),ap(ap(c_2Erelation_2EO(A_27a,A_27c,A_27b),ap(c_2Eset__relation_2Ereln__to__rel(A_27c,A_27b),V14r2)),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27c),V13r1)))) & ((ap(c_2Eset__relation_2Euniv__reln(A_27a),V12s) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Eset__relation_2ERRUNIV(A_27a),V12s))) & ((ap(c_2Eset__relation_2Etc(A_27a),V11r) = ap(c_2Eset__relation_2Erel__to__reln(A_27a,A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))) & ((p(ap(c_2Eset__relation_2Eacyclic(A_27a),V11r)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(c_2Erelation_2ETC(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r))))) & ((p(ap(ap(c_2Eset__relation_2Eirreflexive(A_27a),V11r),V12s)) <=> p(ap(c_2Erelation_2Eirreflexive(A_27a),ap(ap(c_2Epred__set_2EREL__RESTRICT(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)),V12s)))) & ((p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V11r),V12s)) <=> p(ap(c_2Erelation_2Ereflexive(A_27a),ap(ap(c_2Eset__relation_2ERREFL__EXP(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)),V12s)))) & ((p(ap(c_2Eset__relation_2Etransitive(A_27a),V11r)) <=> p(ap(c_2Erelation_2Etransitive(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))) & ((p(ap(c_2Eset__relation_2Eantisym(A_27a),V11r)) <=> p(ap(c_2Erelation_2Eantisymmetric(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))) & ((p(ap(ap(c_2Eset__relation_2Epartial__order(A_27a),V11r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))) & ((p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V11r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EWeakLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))) & (p(ap(ap(c_2Eset__relation_2Estrict__linear__order(A_27a),V11r),c_2Epred__set_2EUNIV(A_27a))) <=> p(ap(c_2Erelation_2EStrongLinearOrder(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V11r)))))))))))))))))))))))))))))))))))))))))))))))))))))))).
tff(conj_thm_2Eset__relation_2Eacyclic__WF,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),V0s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r)),V0s))))) => p(ap(c_2Erelation_2EWF(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V1r))))))))))).
tff(ax_thm_2Eset__relation_2Emaximal__elements__def,axiom,( ! [A_27a:del]: ( ! [V0xs:$i] : (mem(V0xs,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0xs),V1r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f352(A_27a,V0xs,V1r))))))))).
tff(ax_thm_2Eset__relation_2Eminimal__elements__def,axiom,( ! [A_27a:del]: ( ! [V0xs:$i] : (mem(V0xs,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),V1r) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f354(A_27a,V0xs,V1r))))))))).
tff(conj_thm_2Eset__relation_2Eminimal__elements__subset,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1lo:$i] : (mem(V1lo,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1lo)),V0s))))))))).
tff(conj_thm_2Eset__relation_2Eminimal__elements__SWAP,lemma,(( ! [A_27a:del]: ( ! [V0xs:$i] : (mem(V0xs,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),c_2Epair_2ESWAP(A_27a,A_27a)),V1r)) = ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0xs),V1r))))))))).
tff(conj_thm_2Eset__relation_2Emaximal__union,lemma,(( ! [A_27a:del]: ( ! [V0e:$i] : (mem(V0e,A_27a) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2r1:$i] : (mem(V2r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V3r2:$i] : (mem(V3r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V1s),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V2r1),V3r2)))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V1s),V2r1))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V1s),V3r2)))))))))))))))).
tff(conj_thm_2Eset__relation_2Eminimal__union,lemma,(( ! [A_27a:del]: ( ! [V0e:$i] : (mem(V0e,A_27a) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2r1:$i] : (mem(V2r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V3r2:$i] : (mem(V3r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V1s),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V2r1),V3r2)))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V1s),V2r1))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V1s),V3r2)))))))))))))))).
tff(conj_thm_2Eset__relation_2Eminimal__elements__mono,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1r_27:$i] : (mem(V1r_27,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V2xs:$i] : (mem(V2xs,arr(A_27a,bool)) => (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r),V1r_27)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V2xs),V1r_27)),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V2xs),V0r))))))))))))).
tff(conj_thm_2Eset__relation_2Eminimal__elements__rrestrict,lemma,(( ! [A_27a:del]: ( ! [V0xs:$i] : (mem(V0xs,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V1r),V0xs)) = ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0xs),V1r))))))))).
tff(conj_thm_2Eset__relation_2EWF__has__minimal__path,lemma,(( ! [A_27a:del]: ( ! [V0r:$i] : (mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (p(ap(c_2Erelation_2EWF(A_27a),ap(c_2Eset__relation_2Ereln__to__rel(A_27a,A_27a),V0r))) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V2s)) => (? [V3y:$i] : (mem(V3y,A_27a) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V2s),V0r))) & (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V1x)),ap(c_2Eset__relation_2Etc(A_27a),V0r))) | (V3y = V1x)))))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__acyclic__has__maximal,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ((~~ (V0s = c_2Epred__set_2EEMPTY(A_27a))) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) => (? [V2x:$i] : (mem(V2x,A_27a) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),V1r))))))))))))))).
tff(conj_thm_2Eset__relation_2Efinite__acyclic__has__minimal,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ((~~ (V0s = c_2Epred__set_2EEMPTY(A_27a))) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) => (? [V2x:$i] : (mem(V2x,A_27a) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r))))))))))))))).
tff(conj_thm_2Eset__relation_2Emaximal__TC,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ((p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),V0s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r)),V0s))) => (ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),ap(c_2Eset__relation_2Etc(A_27a),V1r)) = ap(ap(c_2Eset__relation_2Emaximal__elements(A_27a),V0s),V1r)))))))))).
tff(conj_thm_2Eset__relation_2Eminimal__TC,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ((p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V1r)),V0s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V1r)),V0s))) => (ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),ap(c_2Eset__relation_2Etc(A_27a),V1r)) = ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r)))))))))).
tff(conj_thm_2Eset__relation_2Efinite__acyclic__has__minimal__path,conjecture,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) & (p(ap(c_2Eset__relation_2Eacyclic(A_27a),V1r)) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s)) & (~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r))))))) => (? [V3y:$i] : (mem(V3y,A_27a) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(ap(c_2Eset__relation_2Eminimal__elements(A_27a),V0s),V1r))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V2x)),ap(c_2Eset__relation_2Etc(A_27a),V1r)))))))))))))))).
