thus ( A is reflexive implies for x being Element of A holds x <= x ) by ORDERS_2:1; :: thesis: ( ( for x being Element of A holds x <= x ) implies A is reflexive )
assume A1: for x being Element of A holds x <= x ; :: thesis: A is reflexive
let x be object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: thesis: ( not x in the carrier of A or [x,x] in the InternalRel of A )
assume x in the carrier of A ; :: thesis: [x,x] in the InternalRel of A
then reconsider x = x as Element of A ;
x <= x by A1;
hence [x,x] in the InternalRel of A ; :: thesis: verum