let L be reflexive RelStr ; :: thesis: id the carrier of L c= the InternalRel of L
for a, b being object st [a,b] in id the carrier of L holds
[a,b] in the InternalRel of L

proof

let a, b be object ; :: thesis: ( [a,b] in id the carrier of L implies [a,b] in the InternalRel of L )
assume [a,b] in id the carrier of L ; :: thesis: [a,b] in the InternalRel of L
then A1: ( a = b & a in the carrier of L ) by RELAT_1:def 10;
the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;
hence [a,b] in the InternalRel of L by A1, RELAT_2:def 1; :: thesis: verum

end;

hence id the carrier of L c= the InternalRel of L by RELAT_1:def 3; :: thesis: verum