P. 41 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opelopabaf 4001*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 3999 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- F/xps   &   |- F/yps   &   |- A e. _V   &   |- B e. _V   &   |- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ( <.A , B >. e. { <.x , y >. | ph } <-> ps)
Theorem	opelopabf 4002*	The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 3999 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)
|- F/xps   &   |- F/ych   &   |- A e. _V   &   |- B e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ( <.A , B >. e. { <.x , y >. | ph } <-> ch)
Theorem	ssopab2 4003	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
|- (A.xA.y(ph -> ps) -> { <.x , y >. | ph } C_ { <.x , y >. | ps })
Theorem	ssopab2b 4004	Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- ( { <.x , y >. | ph } C_ { <.x , y >. | ps } <-> A.xA.y(ph -> ps))
Theorem	ssopab2i 4005	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
|- (ph -> ps)   =>   |- { <.x , y >. | ph } C_ { <.x , y >. | ps }
Theorem	ssopab2dv 4006*	Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
|- (ph -> (ps -> ch))   =>   |- (ph -> { <.x , y >. | ps } C_ { <.x , y >. | ch })
Theorem	eqopab2b 4007	Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.)
|- ( { <.x , y >. | ph } = { <.x , y >. | ps } <-> A.xA.y(ph <-> ps))
Theorem	opabm 4008*	Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.)
|- (E.z z e. { <.x , y >. | ph } <-> E.xE.yph)
Theorem	iunopab 4009*	Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
|- U_z e. A { <.x , y >. | ph } = { <.x , y >. | E.z e. A ph }
2.3.5  Power class of union and intersection
Theorem	pwin 4010	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
|- ~P(A i^i B) = ( ~PA i^i ~PB)
Theorem	pwunss 4011	The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
|- ( ~PA u. ~PB) C_ ~P(A u. B)
Theorem	pwssunim 4012	The power class of the union of two classes is a subset of the union of their power classes, if one class is a subclass of the other. One direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- ((A C_ B \/ B C_ A) -> ~P(A u. B) C_ ( ~PA u. ~PB))
Theorem	pwundifss 4013	Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- (( ~P(A u. B) \ ~PA) u. ~PA) C_ ~P(A u. B)
Theorem	pwunim 4014	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by Jim Kingdon, 30-Sep-2018.)
|- ((A C_ B \/ B C_ A) -> ~P(A u. B) = ( ~PA u. ~PB))
2.3.6  Epsilon and identity relations
Syntax	cep 4015	Extend class notation to include the epsilon relation.
class _E
Syntax	cid 4016	Extend the definition of a class to include identity relation.
class _I
Definition	df-eprel 4017*	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, (A _E B <-> A e. B) when B is a set by epelg 4018. Thus, 5 _E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
|- _E = { <.x , y >. | x e. y }
Theorem	epelg 4018	The epsilon relation and membership are the same. General version of epel 4020. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- (B e. V -> (A _E B <-> A e. B))
Theorem	epelc 4019	The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
|- B e. _V   =>   |- (A _E B <-> A e. B)
Theorem	epel 4020	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
|- (x _E y <-> x e. y)
Definition	df-id 4021*	Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 _I 5 and -. 4 _I 5. (Contributed by NM, 13-Aug-1995.)
|- _I = { <.x , y >. | x = y }
2.3.7  Partial and complete ordering
Syntax	wpo 4022	Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
Syntax	wor 4023	Extend wff notation to include the strict linear ordering predicate. Read: ' R orders A.'
wff R Or A
Definition	df-po 4024*	Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression R Po A means R is a partial order on A. (Contributed by NM, 16-Mar-1997.)
|- ( R Po A <-> A.x e. A A.y e. A A.z e. A (-. x Rx /\ ((x Ry /\ y Rz) -> x Rz)))
Definition	df-iso 4025*	Define the strict linear order predicate. The expression R Or A is true if relationship R orders A. The property x Ry -> (x Rz \/ z Ry) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, x Ry \/ x = y \/ y Rx. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
|- ( R Or A <-> ( R Po A /\ A.x e. A A.y e. A A.z e. A (x Ry -> (x Rz \/ z Ry))))
Theorem	poss 4026	Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|- (A C_ B -> ( R Po B -> R Po A))
Theorem	poeq1 4027	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- ( R = S -> ( R Po A <-> S Po A))
Theorem	poeq2 4028	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
|- (A = B -> ( R Po A <-> R Po B))
Theorem	nfpo 4029	Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F/_x R   &   |- F/_xA   =>   |- F/x R Po A
Theorem	nfso 4030	Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F/_x R   &   |- F/_xA   =>   |- F/x R Or A
Theorem	pocl 4031	Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
|- ( R Po A -> ((B e. A /\ C e. A /\ D e. A) -> (-. B RB /\ ((B R C /\ C R D) -> B R D))))
Theorem	ispod 4032*	Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
|- ((ph /\ x e. A) -> -. x Rx)   &   |- ((ph /\ (x e. A /\ y e. A /\ z e. A)) -> ((x Ry /\ y Rz) -> x Rz))   =>   |- (ph -> R Po A)
Theorem	swopolem 4033*	Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- ((ph /\ (x e. A /\ y e. A /\ z e. A)) -> (x Ry -> (x Rz \/ z Ry)))   =>   |- ((ph /\ ( X e. A /\ Y e. A /\ Z e. A)) -> ( X R Y -> ( X R Z \/ Z R Y)))
Theorem	swopo 4034*	A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ((ph /\ (y e. A /\ z e. A)) -> (y Rz -> -. z Ry))   &   |- ((ph /\ (x e. A /\ y e. A /\ z e. A)) -> (x Ry -> (x Rz \/ z Ry)))   =>   |- (ph -> R Po A)
Theorem	poirr 4035	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
|- (( R Po A /\ B e. A) -> -. B RB)
Theorem	potr 4036	A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
|- (( R Po A /\ (B e. A /\ C e. A /\ D e. A)) -> ((B R C /\ C R D) -> B R D))
Theorem	po2nr 4037	A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
|- (( R Po A /\ (B e. A /\ C e. A)) -> -. (B R C /\ C RB))
Theorem	po3nr 4038	A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
|- (( R Po A /\ (B e. A /\ C e. A /\ D e. A)) -> -. (B R C /\ C R D /\ D RB))
Theorem	po0 4039	Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- R Po (/)
Theorem	pofun 4040*	A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
|- S = { <.x , y >. | X R Y }   &   |- (x = y -> X = Y)   =>   |- (( R Po B /\ A.x e. A X e. B) -> S Po A)
Theorem	sopo 4041	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
|- ( R Or A -> R Po A)
Theorem	soss 4042	Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- (A C_ B -> ( R Or B -> R Or A))
Theorem	soeq1 4043	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- ( R = S -> ( R Or A <-> S Or A))
Theorem	soeq2 4044	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
|- (A = B -> ( R Or A <-> R Or B))
Theorem	sonr 4045	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
|- (( R Or A /\ B e. A) -> -. B RB)
Theorem	sotr 4046	A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
|- (( R Or A /\ (B e. A /\ C e. A /\ D e. A)) -> ((B R C /\ C R D) -> B R D))
Theorem	issod 4047*	An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4025). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- (ph -> R Po A)   &   |- ((ph /\ (x e. A /\ y e. A)) -> (x Ry \/ x = y \/ y Rx))   =>   |- (ph -> R Or A)
Theorem	sowlin 4048	A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)
|- (( R Or A /\ (B e. A /\ C e. A /\ D e. A)) -> (B R C -> (B R D \/ D R C)))
Theorem	so2nr 4049	A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
|- (( R Or A /\ (B e. A /\ C e. A)) -> -. (B R C /\ C RB))
Theorem	so3nr 4050	A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
|- (( R Or A /\ (B e. A /\ C e. A /\ D e. A)) -> -. (B R C /\ C R D /\ D RB))
Theorem	sotricim 4051	One direction of sotritric 4052 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- (( R Or A /\ (B e. A /\ C e. A)) -> (B R C -> -. (B = C \/ C RB)))
Theorem	sotritric 4052	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- R Or A   &   |- ((B e. A /\ C e. A) -> (B R C \/ B = C \/ C RB))   =>   |- ((B e. A /\ C e. A) -> (B R C <-> -. (B = C \/ C RB)))
Theorem	sotritrieq 4053	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- R Or A   &   |- ((B e. A /\ C e. A) -> (B R C \/ B = C \/ C RB))   =>   |- ((B e. A /\ C e. A) -> (B = C <-> -. (B R C \/ C RB)))
Theorem	so0 4054	Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- R Or (/)
2.3.8  Set-like relations
Syntax	wse 4055	Extend wff notation to include the set-like predicate. Read: ' R is set-like on A.'
wff R Se A
Definition	df-se 4056*	Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
|- ( R Se A <-> A.x e. A {y e. A | y Rx } e. _V)
Theorem	seex 4057*	The R-preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
|- (( R Se A /\ B e. A) -> {x e. A | x RB } e. _V)
Theorem	exse 4058	Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
|- (A e. V -> R Se A)
Theorem	sess1 4059	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R C_ S -> ( S Se A -> R Se A))
Theorem	sess2 4060	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- (A C_ B -> ( R Se B -> R Se A))
Theorem	seeq1 4061	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- ( R = S -> ( R Se A <-> S Se A))
Theorem	seeq2 4062	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- (A = B -> ( R Se A <-> R Se B))
Theorem	nfse 4063	Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_x R   &   |- F/_xA   =>   |- F/x R Se A
Theorem	epse 4064	The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
|- _E Se A
2.3.9  Ordinals
Syntax	word 4065	Extend the definition of a wff to include the ordinal predicate.
wff Ord A
Syntax	con0 4066	Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On
Syntax	wlim 4067	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A
Syntax	csuc 4068	Extend class notation to include the successor function.
class suc A
Definition	df-iord 4069*	Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4070 instead for naming consistency with set.mm. (New usage is discouraged.)
|- ( Ord A <-> ( Tr A /\ A.x e. A Tr x))
Theorem	dford3 4070*	Alias for df-iord 4069. Use it instead of df-iord 4069 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
|- ( Ord A <-> ( Tr A /\ A.x e. A Tr x))
Definition	df-on 4071	Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
|- On = {x | Ord x }
Definition	df-ilim 4072	Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42, and then changes A =/= (/) to (/) e. A (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4073 instead for naming consistency with set.mm. (New usage is discouraged.)
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U.A))
Theorem	dflim2 4073	Alias for df-ilim 4072. Use it instead of df-ilim 4072 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
|- ( Lim A <-> ( Ord A /\ (/) e. A /\ A = U.A))
Definition	df-suc 4074	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4115). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
|- suc A = (A u. {A })
Theorem	ordeq 4075	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
|- (A = B -> ( Ord A <-> Ord B))
Theorem	elong 4076	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
|- (A e. V -> (A e. On <-> Ord A))
Theorem	elon 4077	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
|- A e. _V   =>   |- (A e. On <-> Ord A)
Theorem	eloni 4078	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
|- (A e. On -> Ord A)
Theorem	elon2 4079	An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
|- (A e. On <-> ( Ord A /\ A e. _V))
Theorem	limeq 4080	Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- (A = B -> ( Lim A <-> Lim B))
Theorem	ordtr 4081	An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
|- ( Ord A -> Tr A)
Theorem	ordelss 4082	An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
|- (( Ord A /\ B e. A) -> B C_ A)
Theorem	trssord 4083	A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
|- (( Tr A /\ A C_ B /\ Ord B) -> Ord A)
Theorem	ordelord 4084	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
|- (( Ord A /\ B e. A) -> Ord B)
Theorem	tron 4085	The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
|- Tr On
Theorem	ordelon 4086	An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
|- (( Ord A /\ B e. A) -> B e. On)
Theorem	onelon 4087	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
|- ((A e. On /\ B e. A) -> B e. On)
Theorem	ordin 4088	The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
|- (( Ord A /\ Ord B) -> Ord (A i^i B))
Theorem	onin 4089	The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
|- ((A e. On /\ B e. On) -> (A i^i B) e. On)
Theorem	onelss 4090	An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- (A e. On -> (B e. A -> B C_ A))
Theorem	ordtr1 4091	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
|- ( Ord C -> ((A e. B /\ B e. C) -> A e. C))
Theorem	ontr1 4092	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
|- ( C e. On -> ((A e. B /\ B e. C) -> A e. C))
Theorem	onintss 4093*	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
|- (x = A -> (ph <-> ps))   =>   |- (A e. On -> (ps -> |^| {x e. On | ph } C_ A))
Theorem	ord0 4094	The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
|- Ord (/)
Theorem	0elon 4095	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
|- (/) e. On
Theorem	inton 4096	The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
|- |^| On = (/)
Theorem	nlim0 4097	The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
|- -. Lim (/)
Theorem	limord 4098	A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
|- ( Lim A -> Ord A)
Theorem	limuni 4099	A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
|- ( Lim A -> A = U.A)
Theorem	limuni2 4100	The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
|- ( Lim A -> Lim U.A)