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 set ; :: 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 set such that
A2: ( y1 in B & y2 in A & y = [y1,y2] ) by ZFMISC_1:def 2;
A3: [y2,y1] in [:A,B:] by A2, ZFMISC_1:106;
<:(pr2 X,Y),(pr1 X,Y):> . y2,y1 = [y1,y2] by A2, Lm1;
hence y in <:(pr2 X,Y),(pr1 X,Y):> .: [:A,B:] by A1, A2, A3, FUNCT_1:def 12; :: thesis: verum