let x1, y1, x2, y2 be set ; :: thesis: ( not {[x1,y1],[x2,y2]} is FinSequence or ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
assume {[x1,y1],[x2,y2]} is FinSequence ; :: thesis: ( ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
then reconsider p = {[x1,y1],[x2,y2]} as FinSequence ;
dom p = {x1,x2} by RELAT_1:24;
then A1: ( x1 in dom p & x2 in dom p ) by TARSKI:def 2;
( [x1,y1] in p & [x2,y2] in p ) by TARSKI:def 2;
then A2: ( p . x1 = y1 & p . x2 = y2 ) by FUNCT_1:8;
A3: dom p = Seg (len p) by FINSEQ_1:def 3;
A4: len p <= 1 + 1 by CARD_2:69;
len p > 0 by NAT_1:3;
then A5: len p >= 0 + 1 by NAT_1:13;

A6: now

assume len p = 1 ; :: thesis: ( x1 = 1 & x2 = 1 & y1 = y2 )
hence ( x1 = 1 & x2 = 1 ) by A1, A3, FINSEQ_1:4, TARSKI:def 1; :: thesis: y1 = y2
hence y1 = y2 by A2; :: thesis: verum

end;

now

assume A7: len p = 2 ; :: thesis: ( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
A8: ( x1 = x2 implies p = {[x1,y1]} ) by A2, ENUMSET1:69;
( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 1 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A1, A3, A7, FINSEQ_1:4, TARSKI:def 2;
hence ( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) ) by A7, A8, CARD_1:50; :: thesis: verum

end;

hence ( ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) ) by A4, A5, A6, NAT_1:9; :: thesis: verum