let A, B, X, Y 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 object ; :: 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 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; :: thesis: verum