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

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

proof

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

end;proof

thus
{ n where n is Nat : n is even } c= EvenNAT
:: thesis: verum
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;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

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

( b