now :: thesis: for x being object holds
( ( x in Seg 1 implies x in {1} ) & ( x in {1} implies x in Seg 1 ) )

let x be object ; :: thesis: ( ( x in Seg 1 implies x in {1} ) & ( x in {1} implies x in Seg 1 ) )
thus ( x in Seg 1 implies x in {1} ) :: thesis: ( x in {1} implies x in Seg 1 )

proof

assume x in Seg 1 ; :: thesis: x in {1}
then consider k being Nat such that
A1: x = k and
A2: ( 1 <= k & k <= 1 ) ;
k = 1 by A2, XXREAL_0:1;
hence x in {1} by A1, TARSKI:def 1; :: thesis: verum

end;

assume x in {1} ; :: thesis: x in Seg 1
then x = 1 by TARSKI:def 1;
hence x in Seg 1 ; :: thesis: verum

end;

hence Seg 1 = {1} by TARSKI:2; :: thesis: Seg 2 = {1,2}

now :: thesis: for x being object holds
( ( x in Seg 2 implies x in {1,2} ) & ( x in {1,2} implies x in Seg 2 ) )

let x be object ; :: thesis: ( ( x in Seg 2 implies x in {1,2} ) & ( x in {1,2} implies x in Seg 2 ) )
thus ( x in Seg 2 implies x in {1,2} ) :: thesis: ( x in {1,2} implies x in Seg 2 )

proof

assume x in Seg 2 ; :: thesis: x in {1,2}
then consider k being Nat such that
A3: x = k and
A4: 1 <= k and
A5: k <= 2 ;
k <= 1 + 1 by A5;
then ( k = 1 or k = 2 ) by A4, NAT_1:9;
hence x in {1,2} by A3, TARSKI:def 2; :: thesis: verum

end;

assume x in {1,2} ; :: thesis: x in Seg 2
then ( x = 1 or x = 2 ) by TARSKI:def 2;
hence x in Seg 2 ; :: thesis: verum

end;

hence Seg 2 = {1,2} by TARSKI:2; :: thesis: verum