let CS be CongrSpace; the CONGR of CS is_reflexive_in [: the carrier of CS, the carrier of CS:]
let x be object ; RELAT_2:def 1 ( 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:]
; [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; verum