let A be non empty set ; :: thesis: for R being Relation of [:A,A:] st R is_reflexive_in [:A,A:] holds

id A is_FormalIz_of R

let R be Relation of [:A,A:]; :: thesis: ( R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R )

assume A1: for x being object st x in [:A,A:] holds

[x,x] in R ; :: according to RELAT_2:def 1 :: thesis: id A is_FormalIz_of R

let x be Element of A; :: according to TRANSGEO:def 2 :: thesis: for y being Element of A holds [[x,y],[((id A) . x),((id A) . y)]] in R

let y be Element of A; :: thesis: [[x,y],[((id A) . x),((id A) . y)]] in R

A2: [x,y] in [:A,A:] by ZFMISC_1:def 2;

thus [[x,y],[((id A) . x),((id A) . y)]] in R by A1, A2; :: thesis: verum

id A is_FormalIz_of R

let R be Relation of [:A,A:]; :: thesis: ( R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R )

assume A1: for x being object st x in [:A,A:] holds

[x,x] in R ; :: according to RELAT_2:def 1 :: thesis: id A is_FormalIz_of R

let x be Element of A; :: according to TRANSGEO:def 2 :: thesis: for y being Element of A holds [[x,y],[((id A) . x),((id A) . y)]] in R

let y be Element of A; :: thesis: [[x,y],[((id A) . x),((id A) . y)]] in R

A2: [x,y] in [:A,A:] by ZFMISC_1:def 2;

thus [[x,y],[((id A) . x),((id A) . y)]] in R by A1, A2; :: thesis: verum