theorem nflower {x: nat} (A: set x): $ FS/ x A $ > $ FN/ x lower A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsv | FS/ x a1 |
|
2 | hyp h | FS/ x A |
|
3 | 1, 2 | nfeqs | F/ x a1 == A |
4 | 3 | nfab | FS/ x {a1 | a1 == A} |
5 | 4 | nfthe | FN/ x the {a1 | a1 == A} |
6 | 5 | conv lower | FN/ x lower A |