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):>;
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
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 12;
consider x1, x2 being set 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:106;
then <:(pr2 X,Y),(pr1 X,Y):> . x1,x2 = [x2,x1] by Lm1;
hence y in [:B,A:] by A3, A4, A5, ZFMISC_1:106; :: thesis: verum