let p1, p2 be set ; :: thesis: ( p1 <> p2 implies p2 .. <*p1,p2*> = 2 )
assume A1:
p1 <> p2
; :: thesis: p2 .. <*p1,p2*> = 2
2 <= len <*p1,p2*>
by FINSEQ_1:61;
then A2:
2 in dom <*p1,p2*>
by FINSEQ_3:27;
A3:
<*p1,p2*> . 2 = p2
by FINSEQ_1:61;
A4:
<*p1,p2*> . 1 = p1
by FINSEQ_1:61;
now let i be
Nat;
:: thesis: ( 1 <= i & i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 )assume A5:
1
<= i
;
:: thesis: ( i < 1 + 1 implies <*p1,p2*> . i <> <*p1,p2*> . 2 )assume
i < 1
+ 1
;
:: thesis: <*p1,p2*> . i <> <*p1,p2*> . 2then
i <= 1
by NAT_1:13;
hence
<*p1,p2*> . i <> <*p1,p2*> . 2
by A1, A3, A4, A5, XXREAL_0:1;
:: thesis: verum end;
hence
p2 .. <*p1,p2*> = 2
by A2, A3, Th4; :: thesis: verum