let A be RelStr ; :: thesis: for a1, a2 being Element of A st a1 <= a2 holds
( a1 in the carrier of A & a2 in the carrier of A )
let a1, a2 be Element of A; :: thesis: ( a1 <= a2 implies ( a1 in the carrier of A & a2 in the carrier of A ) )
assume a1 <= a2 ; :: thesis: ( a1 in the carrier of A & a2 in the carrier of A )
then [a1,a2] in the InternalRel of A by ORDERS_2:def 5;
hence ( a1 in the carrier of A & a2 in the carrier of A ) by ZFMISC_1:87; :: thesis: verum