theorem nfss {x: nat} (A B: set x): $ FS/ x A $ > $ FS/ x B $ > $ F/ x A C_ B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h1 | FS/ x A |
|
| 2 | 1 | nfel2 | F/ x y e. A |
| 3 | hyp h2 | FS/ x B |
|
| 4 | 3 | nfel2 | F/ x y e. B |
| 5 | 2, 4 | nfim | F/ x y e. A -> y e. B |
| 6 | 5 | nfal | F/ x A. y (y e. A -> y e. B) |
| 7 | 6 | conv subset | F/ x A C_ B |