let A be non empty reflexive RelStr ; :: thesis: for a being Element of A holds a <= a
let a be Element of A; :: thesis: a <= a
the InternalRel of A is_reflexive_in the carrier of A by Def4;
then [a,a] in the InternalRel of A by RELAT_2:def 1;
hence a <= a by Def9; :: thesis: verum