set f = PrimeNumbersS s;
let m, n be Nat; :: according to SEQM_3:def 1 :: thesis: ( not m in proj1 (PrimeNumbersS s) or not n in proj1 (PrimeNumbersS s) or n <= m or not (PrimeNumbersS s) . n <= (PrimeNumbersS s) . m )
( (PrimeNumbersS s) . m = primenumber m & (PrimeNumbersS s) . n = primenumber n ) by Def3;
hence ( not m in proj1 (PrimeNumbersS s) or not n in proj1 (PrimeNumbersS s) or n <= m or not (PrimeNumbersS s) . n <= (PrimeNumbersS s) . m ) by MOEBIUS2:21; :: thesis: verum