theorem ssri2 (A B: set) {x y: nat}: $ x, y e. A -> x, y e. B $ > $ A C_ B $;
x, y e. A -> x, y e. B
T. -> x, y e. A -> x, y e. B
T. -> A C_ B
A C_ B