let A, B, X, Y be set ; <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] c= [:B,A:]
set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>;
let y be object ; TARSKI:def 3 ( not y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] or y in [:B,A:] )
assume
y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:]
; y in [:B,A:]
then consider x being object such that
A1:
x in dom <:(pr2 (X,Y)),(pr1 (X,Y)):>
and
A2:
x in [:A,B:]
and
A3:
y = <:(pr2 (X,Y)),(pr1 (X,Y)):> . x
by FUNCT_1:def 6;
consider x1, x2 being object such that
A4:
( x1 in A & x2 in B )
and
A5:
x = [x1,x2]
by A2, ZFMISC_1:def 2;
dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:]
by Th4;
then
( x1 in X & x2 in Y )
by A1, A5, ZFMISC_1:87;
then
<:(pr2 (X,Y)),(pr1 (X,Y)):> . (x1,x2) = [x2,x1]
by Lm1;
hence
y in [:B,A:]
by A3, A4, A5, ZFMISC_1:87; verum