A1: 0_No in {0_No} by TARSKI:def 1;
assume 1_No <= 0_No ; :: according to SURREALI:def 8 :: thesis: contradiction
then L_ 1_No << {0_No} by SURREAL0:43;
hence contradiction by SURREALO:3, A1; :: thesis: verum