(2,4,7,8) prove (9), and (9) proves (10).

(2) (x = x)euivalent (x = x.X)

(4) (x = x.X)euivalent(x cont x & x emb X)

(7) (x cont x)euivalent ((x ex X) & (x = x))

(8) (x emb X) euivalent ((x ex X) & (X = X))

(9) (x = x)euivalent((x ex X) & (x = x) & (X = X))

(10) (x = x) if-then (x ex X)