A3: { n where n is Nat : ( n in dom f & f . n < Mean f ) } c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Nat : ( n in dom f & f . n < Mean f ) } or x in dom f )
assume x in { n where n is Nat : ( n in dom f & f . n < Mean f ) } ; :: thesis: x in dom f
then consider n being Nat such that
A2: ( x = n & n in dom f & f . n < Mean f ) ;
thus x in dom f by A2; :: thesis: verum

end;

dom f c= NAT ;
then { n where n is Nat : ( n in dom f & f . n < Mean f ) } c= NAT by A3;
hence { n where n is Nat : ( n in dom f & f . n < Mean f ) } is Subset of NAT ; :: thesis: verum