let CS be CongrSpace; :: thesis: the CONGR of CS is_symmetric_in [: the carrier of CS, the carrier of CS:]

let x, y be object ; :: 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:] and

A2: y in [: the carrier of CS, the carrier of CS:] and

A3: [x,y] in the CONGR of CS ; :: thesis: [y,x] in the CONGR of CS

consider x1, x2 being Element of CS such that

A4: x = [x1,x2] by A1, DOMAIN_1:1;

consider y1, y2 being Element of CS such that

A5: y = [y1,y2] by A2, DOMAIN_1:1;

x1,x2 // y1,y2 by A3, A4, A5, ANALOAF:def 2;

then y1,y2 // x1,x2 by Def5;

hence [y,x] in the CONGR of CS by A4, A5, ANALOAF:def 2; :: thesis: verum

let x, y be object ; :: 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:] and

A2: y in [: the carrier of CS, the carrier of CS:] and

A3: [x,y] in the CONGR of CS ; :: thesis: [y,x] in the CONGR of CS

consider x1, x2 being Element of CS such that

A4: x = [x1,x2] by A1, DOMAIN_1:1;

consider y1, y2 being Element of CS such that

A5: y = [y1,y2] by A2, DOMAIN_1:1;

x1,x2 // y1,y2 by A3, A4, A5, ANALOAF:def 2;

then y1,y2 // x1,x2 by Def5;

hence [y,x] in the CONGR of CS by A4, A5, ANALOAF:def 2; :: thesis: verum