theorem :: ORDINAL3:15

1 = {{}} by Lm1;