hereby :: thesis: ( Seg 1 = {1} & Seg 2 = {1,2} )

consider x being Element of Seg 0 ;
assume A1: Seg 0 <> {} ; :: thesis: contradiction
then reconsider x = x as Element of NAT by TARSKI:def 3;
( 1 <= x & x <= 0 ) by A1, Th3;
hence contradiction ; :: thesis: verum

end;

now

let x be set ; :: 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 Element of NAT such that
A2: ( x = k & 1 <= k & k <= 1 ) ;
k = 1 by A2, XXREAL_0:1;
hence x in {1} by A2, 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

let x be set ; :: 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 Element of NAT such that
A3: ( x = k & 1 <= k & k <= 2 ) ;
k <= 1 + 1 by A3;
then ( k = 1 or k = 2 ) by A3, 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