let CS be CongrSpace; :: thesis: the CONGR of CS is_reflexive_in [:the carrier of CS,the carrier of CS:]
let x be set ; :: 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:9;
x1,x2 // x1,x2 by Def5;
hence [x,x] in the CONGR of CS by A1, ANALOAF:def 2; :: thesis: verum