EvenNAT = { n where n is Nat : n is even }

proof

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

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in EvenNAT or m in { n where n is Nat : n is even } )
assume m in EvenNAT ; :: thesis: m in { n where n is Nat : n is even }
then consider k being Nat such that
A1: m = 2 * k by FIB_NUM2:def 3;
thus m in { n where n is Nat : n is even } by A1; :: thesis: verum

end;

thus { n where n is Nat : n is even } c= EvenNAT :: thesis: verum

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in { n where n is Nat : n is even } or m in EvenNAT )
assume m in { n where n is Nat : n is even } ; :: thesis: m in EvenNAT
then consider n being Nat such that
A2: ( n = m & n is even ) ;
consider k being Nat such that
A3: n = 2 * k by A2, ABIAN:def 2;
thus m in EvenNAT by A2, A3, FIB_NUM2:def 3; :: thesis: verum

end;

end;

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