OddNAT = { n where n is Nat : n is odd }
_{1} being Element of K37(omega) holds

( b_{1} = OddNAT iff b_{1} = { n where n is Nat : n is odd } )
; :: thesis: verum

proof

hence
for b
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

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;proof

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 )
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;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

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

( b