set S = { [n,(n + 1)] where n is Nat : verum } ;

now :: thesis: for z being object holds
( ( z in succRel omega implies z in { [n,(n + 1)] where n is Nat : verum } ) & ( z in { [n,(n + 1)] where n is Nat : verum } implies z in succRel omega ) )

let z be object ; :: thesis: ( ( z in succRel omega implies z in { [n,(n + 1)] where n is Nat : verum } ) & ( z in { [n,(n + 1)] where n is Nat : verum } implies z in succRel omega ) )

hereby :: thesis: ( z in { [n,(n + 1)] where n is Nat : verum } implies z in succRel omega )

assume A0: z in succRel omega ; :: thesis: z in { [n,(n + 1)] where n is Nat : verum }
then consider x, y being object such that
A0a: z = [x,y] by RELAT_1:def 1;
reconsider a = x, b = y as set by TARSKI:1;
[a,b] in succRel omega by A0, A0a;
then A1: ( a in omega & b in omega & b = succ a ) by Def1;
then reconsider a = a, b = b as Nat ;
b = succ (Segm a) by A1, ORDINAL1:def 17
.= Segm (a + 1) by NAT_1:38
.= a + 1 by ORDINAL1:def 17 ;
hence z in { [n,(n + 1)] where n is Nat : verum } by A0a; :: thesis: verum

end;

assume z in { [n,(n + 1)] where n is Nat : verum } ; :: thesis: z in succRel omega
then consider n being Nat such that
A2: z = [n,(n + 1)] ;
A4: n + 1 = Segm (n + 1) by ORDINAL1:def 17
.= succ (Segm n) by NAT_1:38
.= succ n by ORDINAL1:def 17 ;
( n in omega & n + 1 in omega ) by ORDINAL1:def 12;
hence z in succRel omega by A2, A4, Def1; :: thesis: verum

end;

hence succRel omega = { [n,(n + 1)] where n is Nat : verum } by TARSKI:2; :: thesis: verum