let CS be CongrSpace; :: thesis: the CONGR of CS is_symmetric_in [:the carrier of CS,the carrier of CS:]
let x, y be set ; :: according to RELAT_2:def 3 :: thesis: ( not x in [:the carrier of CS,the carrier of CS:] or not y in [:the carrier of CS,the carrier of CS:] or not [x,y] in the CONGR of CS or [y,x] in the CONGR of CS )
assume that
A1: ( x in [:the carrier of CS,the carrier of CS:] & y in [:the carrier of CS,the carrier of CS:] ) and
A2: [x,y] in the CONGR of CS ; :: thesis: [y,x] in the CONGR of CS
consider x1, x2 being Element of CS such that
A3: x = [x1,x2] by A1, DOMAIN_1:9;
consider y1, y2 being Element of CS such that
A4: y = [y1,y2] by A1, DOMAIN_1:9;
x1,x2 // y1,y2 by A2, A3, A4, ANALOAF:def 2;
then y1,y2 // x1,x2 by Def5;
hence [y,x] in the CONGR of CS by A3, A4, ANALOAF:def 2; :: thesis: verum