let f be Function; :: thesis: for O being non empty connected Poset
for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let O be non empty connected Poset; :: thesis: for T being non empty array of O
for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let T be non empty array of O; :: thesis: for p, q being Element of dom T st p in q & f = (T,p,q) incl holds
for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
let p, q be Element of dom T; :: thesis: ( p in q & f = (T,p,q) incl implies for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 ) )
assume Z0: ( p in q & f = (T,p,q) incl ) ; :: thesis: for x1, x2, y1, y2 being Element of dom T st x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) holds
( x1 = x2 & y1 = y2 )
then Z1: p <> q ;
let x1, x2, y1, y2 be Element of dom T; :: thesis: ( x1 in y1 & x2 in y2 & f . (x1,y1) = f . (x2,y2) implies ( x1 = x2 & y1 = y2 ) )
assume that
Z2: ( x1 in y1 & x2 in y2 ) and
Z4: f . (x1,y1) = f . (x2,y2) ; :: thesis: ( x1 = x2 & y1 = y2 )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);

per cases ( ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) or ( x1 = p & y1 in q ) or ( x1 = p & y1 = q ) or ( p in x1 & y1 = q ) or ( x1 in p & y1 = p ) or ( x1 in p & y1 = q ) or ( x1 = p & q in y1 ) or ( x1 = q & q in y1 ) ) by Z0, Z2, Eight;

suppose C1: ( x1 <> p & x1 <> q & y1 <> p & y1 <> q ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [x1,y1] by Z0, Case1;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,q] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,p] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [q,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [p,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

suppose C1: ( x1 = p & y1 in q ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [x1,y1] by Z0, Z2, Case47;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,q] & x2 <> p ) by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,p] & x2 <> p ) by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [q,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z1, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [p,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C1, C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

suppose C1: ( x1 = p & y1 = q ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [x1,y1] by Z0, Case5;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,q] & x2 <> p ) by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,p] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by Z1, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [q,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z1, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [p,y2] & y2 <> q ) by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

suppose C1: ( p in x1 & y1 = q ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [x1,y1] by Z0, Z2, Case47;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,q] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C2, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,p] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C2, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [q,y2] & y2 <> q ) by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [p,y2] & y2 <> q ) by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

suppose C1: ( x1 in p & y1 = p ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [x1,q] by Z0, Case23;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose C2: S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,q] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C2, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,p] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by Z1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by C1, Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,y2] & x2 <> x1 ) by C1, Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [q,y2] & y2 <> q ) by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by C1, C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [p,y2] & x1 <> p ) by C1, Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

suppose C1: ( x1 in p & y1 = q ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [x1,p] by Z0, Case23;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose C2: S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,q] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by Z1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,p] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by C2, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,y2] & x1 <> p ) by C1, Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by C2, Z1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [q,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z0, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z1, C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [p,y2] & x1 <> p ) by C1, Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

suppose C1: ( x1 = p & q in y1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [q,y1] by Z0, Case68;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose C2: S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,q] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by Z0, C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,p] by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by Z0, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,y2] & x2 <> q ) by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by Z1, C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [q,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C2, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,y2] & x2 <> q ) by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [p,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

suppose C1: ( x1 = q & q in y1 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

then D1: f . (x1,y1) = [p,y1] by Z0, Case68;

per cases ( S₁[p,q,x2,y2] or S₂[p,q,x2,y2] or S₃[p,q,x2,y2] or S₄[p,q,x2,y2] or S₅[p,q,x2,y2] or S₆[p,q,x2,y2] or S₇[p,q,x2,y2] or S₈[p,q,x2,y2] ) by Z0, Z2, Eight;

suppose C2: S₁[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Case1;
hence ( x1 = x2 & y1 = y2 ) by C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₂[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,q] & p <> x2 ) by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₃[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,p] & p <> x2 ) by Z0, Case23;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₄[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [x2,y2] by Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by C1, C2, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₅[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,y2] & y1 <> y2 ) by C1, Z0, Case5;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₆[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [q,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by Z1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose S₇[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then ( f . (x2,y2) = [x2,y2] & y2 <> y1 ) by C1, Z0, Z2, Case47;
hence ( x1 = x2 & y1 = y2 ) by Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

suppose C2: S₈[p,q,x2,y2] ; :: thesis: ( x1 = x2 & y1 = y2 )

then f . (x2,y2) = [p,y2] by Z0, Case68;
hence ( x1 = x2 & y1 = y2 ) by C2, C1, Z4, D1, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

end;