Description: Lemma for nsgqusf1o . (Contributed by Thierry Arnoux, 4-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nsgqusf1o.b | |
|
nsgqusf1o.s | |
||
nsgqusf1o.t | |
||
nsgqusf1o.1 | |
||
nsgqusf1o.2 | No typesetting found for |- .c_ = ( le ` ( toInc ` T ) ) with typecode |- | ||
nsgqusf1o.q | |
||
nsgqusf1o.p | |
||
nsgqusf1o.e | |
||
nsgqusf1o.f | |
||
nsgqusf1o.n | |
||
Assertion | nsgqusf1olem1 | |