let X, Y, A, B be set ; :: thesis: <:(pr2 X,Y),(pr1 X,Y):> .: [:A,B:] c= [:B,A:]
set f = <:(pr2 X,Y),(pr1 X,Y):>;
A1: dom <:(pr2 X,Y),(pr1 X,Y):> = [:X,Y:] by Th4;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( 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:] ; :: thesis: y in [:B,A:]
then consider x being set such that
A2: ( x in dom <:(pr2 X,Y),(pr1 X,Y):> & x in [:A,B:] & y = <:(pr2 X,Y),(pr1 X,Y):> . x ) by FUNCT_1:def 12;
consider x1, x2 being set such that
A3: ( x1 in A & x2 in B & x = [x1,x2] ) by A2, ZFMISC_1:def 2;
( x1 in X & x2 in Y ) by A1, A2, A3, ZFMISC_1:106;
then <:(pr2 X,Y),(pr1 X,Y):> . x1,x2 = [x2,x1] by Lm1;
hence y in [:B,A:] by A2, A3, ZFMISC_1:106; :: thesis: verum