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