let x, y be set ; :: thesis: for k being natural number st Seg k = {x,y} & x <> y holds
( k = 2 & {x,y} = {1,2} )
let k be natural number ; :: thesis: ( Seg k = {x,y} & x <> y implies ( k = 2 & {x,y} = {1,2} ) )
assume that
A1: Seg k = {x,y} and
A2: x <> y ; :: thesis: ( k = 2 & {x,y} = {1,2} )

now

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: ( k = 2 & {x,y} = {1,2} )

hence ( k = 2 & {x,y} = {1,2} ) by A1; :: thesis: verum

end;

suppose A3: k <> 0 ; :: thesis: ( k = 2 & {x,y} = {1,2} )

now

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: ( k = 2 & {x,y} = {1,2} )

hence ( k = 2 & {x,y} = {1,2} ) by A1, A2, FINSEQ_1:4, ZFMISC_1:9; :: thesis: verum

end;

suppose A4: k <> 1 ; :: thesis: ( k = 2 & {x,y} = {1,2} )

1 <= k by A3, NAT_1:14;
then 1 < k by A4, XXREAL_0:1;
then A5: 1 + 1 <= k by NAT_1:13;
then Seg 2 c= Seg k by FINSEQ_1:7;
then A6: ( ( 1 = x & 2 = x ) or ( 1 = x & 2 = y ) or ( 2 = x & 1 = y ) or ( 1 = y & 2 = y ) ) by A1, FINSEQ_1:4, ZFMISC_1:28;

now

assume A7: not k <= 2 ; :: thesis: contradiction
k in Seg k by A1, FINSEQ_1:4, FINSEQ_1:5;
then ( ( k = 1 or k = 2 ) & 1 <= 3 & 2 <= 3 ) by A1, A6, TARSKI:def 2;
hence contradiction by A7; :: thesis: verum

end;

hence ( k = 2 & {x,y} = {1,2} ) by A1, A5, FINSEQ_1:4, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ( k = 2 & {x,y} = {1,2} ) ; :: thesis: verum

end;

end;

end;

hence ( k = 2 & {x,y} = {1,2} ) ; :: thesis: verum