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
a <= a ;
hence a =~ a ; :: thesis: verum