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

( 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