let x, y be object ; :: thesis: for k being Nat st Seg k = {x,y} & x <> y holds
( k = 2 & {x,y} = {1,2} )
let k be Nat; :: 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 :: thesis: ( k = 2 & {x,y} = {1,2} )
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 :: thesis: ( k = 2 & {x,y} = {1,2} )
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:2, ZFMISC_1:5; :: 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:5;
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:2, ZFMISC_1:22;
now :: thesis: k <= 2
k in Seg k by A1, Th7;
then A7: ( k = 1 or k = 2 ) by A1, A6, TARSKI:def 2;
assume not k <= 2 ; :: thesis: contradiction
hence contradiction by A7; :: thesis: verum
end;
hence ( k = 2 & {x,y} = {1,2} ) by A1, A5, FINSEQ_1:2, 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