OddNAT = { n where n is Nat : n is odd }

proof

thus OddNAT c= { n where n is Nat : n is odd } :: according to XBOOLE_0:def 10 :: thesis: { n where n is Nat : n is odd } c= OddNAT

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in OddNAT or m in { n where n is Nat : n is odd } )
assume m in OddNAT ; :: thesis: m in { n where n is Nat : n is odd }
then consider k being Element of NAT such that
A1: m = (2 * k) + 1 by FIB_NUM2:def 4;
thus m in { n where n is Nat : n is odd } by A1; :: thesis: verum

end;

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in { n where n is Nat : n is odd } or m in OddNAT )
assume m in { n where n is Nat : n is odd } ; :: thesis: m in OddNAT
then consider n being Nat such that
A2: ( n = m & n is odd ) ;
consider k being Nat such that
A3: n = (2 * k) + 1 by A2, ABIAN:9;
k is Element of NAT by ORDINAL1:def 12;
hence m in OddNAT by A2, A3, FIB_NUM2:def 4; :: thesis: verum

end;

hence for b₁ being Element of K37(omega) holds
( b₁ = OddNAT iff b₁ = { n where n is Nat : n is odd } ) ; :: thesis: verum