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

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in [: the carrier of CS, the carrier of CS:] or [x,x] in the CONGR of CS )

assume x in [: the carrier of CS, the carrier of CS:] ; :: thesis: [x,x] in the CONGR of CS

then consider x1, x2 being Element of CS such that

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

x1,x2 // x1,x2 by Def5;

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

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in [: the carrier of CS, the carrier of CS:] or [x,x] in the CONGR of CS )

assume x in [: the carrier of CS, the carrier of CS:] ; :: thesis: [x,x] in the CONGR of CS

then consider x1, x2 being Element of CS such that

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

x1,x2 // x1,x2 by Def5;

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