theorem Th12: :: TRANSGEO:12

for A being non empty set
for R being Relation of [:A,A:] st R is_reflexive_in [:A,A:] holds
id A is_FormalIz_of R