let X, Y be set ; :: thesis: for A being Subset of X
for B being Subset of Y holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:]
let A be Subset of X; :: thesis: for B being Subset of Y holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:]
let B be Subset of Y; :: thesis: <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:]
set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>;
A1: dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] by Th4;
thus <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] c= [:B,A:] by Th5; :: according to XBOOLE_0:def 10 :: thesis: [:B,A:] c= <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:]
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [:B,A:] or y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] )
assume y in [:B,A:] ; :: thesis: y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:]
then consider y1, y2 being object such that
A2: ( y1 in B & y2 in A ) and
A3: y = [y1,y2] by ZFMISC_1:def 2;
( [y2,y1] in [:A,B:] & <:(pr2 (X,Y)),(pr1 (X,Y)):> . (y2,y1) = [y1,y2] ) by A2, Lm1, ZFMISC_1:87;
hence y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] by A1, A3, FUNCT_1:def 6; :: thesis: verum