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

let a be Element of A; :: thesis: a =~ a

a <= a ;

hence a =~ a ; :: thesis: verum