theorem dfss (A B: set) {x: nat}: $ A C_ B <-> A. x (x e. A -> x e. B) $;
A C_ B <-> A C_ B
A C_ B <-> A. x (x e. A -> x e. B)