let W be Universe; :: thesis: ( omega in W implies W |= the_axiom_of_infinity )
assume omega in W ; :: thesis: W |= the_axiom_of_infinity
then reconsider u = omega as Element of W ;

now

take u = u; :: thesis: ( u <> {} & ( for v being Element of W st v in u holds
ex w being Element of W st
( v c< w & w in u ) ) )
thus u <> {} ; :: thesis: for v being Element of W st v in u holds
ex w being Element of W st
( v c< w & w in u )
let v be Element of W; :: thesis: ( v in u implies ex w being Element of W st
( v c< w & w in u ) )
assume A1: v in u ; :: thesis: ex w being Element of W st
( v c< w & w in u )
then reconsider A = v as Ordinal ;
A2: omega is limit_ordinal by ORDINAL1:def 12;
then succ A in omega by A1, ORDINAL1:41;
then succ A c= u by ORDINAL1:def 2;
then reconsider w = succ A as Element of W by CLASSES1:def 1;
take w = w; :: thesis: ( v c< w & w in u )
A in succ A by ORDINAL1:10;
then ( v c= w & v <> w ) by ORDINAL1:def 2;
hence ( v c< w & w in u ) by A1, A2, ORDINAL1:41, XBOOLE_0:def 8; :: thesis: verum

end;

hence W |= the_axiom_of_infinity by ZFMODEL1:6; :: thesis: verum