thus ( A is reflexive implies for x being Element of A holds x <= x ) by ORDERS_2:24; :: 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 set ; :: according to RELAT_2:def 1,ORDERS_2:def 4 :: 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 by ORDERS_2:def 9; :: thesis: verum