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 Def2;
then [a,a] in the InternalRel of A ;
hence a <= a ; :: thesis: verum