let p1, p2 be set ; ( p1 <> p2 implies p2 .. <*p1,p2*> = 2 )
A1:
<*p1,p2*> . 2 = p2
by FINSEQ_1:44;
A2:
<*p1,p2*> . 1 = p1
by FINSEQ_1:44;
assume A3:
p1 <> p2
; p2 .. <*p1,p2*> = 2
A4:
now for i being Nat st 1 <= i & i < 1 + 1 holds
<*p1,p2*> . i <> <*p1,p2*> . 2let i be
Nat;
( 1 <= i & i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 )assume A5:
1
<= i
;
( i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 )assume
i < 1
+ 1
;
<*p1,p2*> . i <> <*p1,p2*> . 2then
i <= 1
by NAT_1:13;
hence
<*p1,p2*> . i <> <*p1,p2*> . 2
by A3, A1, A2, A5, XXREAL_0:1;
verum end;
2 <= len <*p1,p2*>
by FINSEQ_1:44;
then
2 in dom <*p1,p2*>
by FINSEQ_3:25;
hence
p2 .. <*p1,p2*> = 2
by A1, A4, Th2; verum