let i, j be Element of (F opp+id ); :: according to WAYBEL21:def 2 :: thesis: ( i <= j implies (F opp+id ) . i >= (F opp+id ) . j )
A1: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
then reconsider x = i, y = j as Element of (T opp ) by YELLOW_0:59;
assume i <= j ; :: thesis: (F opp+id ) . i >= (F opp+id ) . j
then x <= y by A1, YELLOW_0:60;
then ( ~ x >= ~ y & ~ x = x ) by YELLOW_7:1;
then ( (F opp+id ) . i >= ~ y & ~ y = y ) by YELLOW_9:7;
hence (F opp+id ) . i >= (F opp+id ) . j by YELLOW_9:7; :: thesis: verum