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:58;
assume i <= j ; :: thesis: (F opp+id) . i >= (F opp+id) . j
then x <= y by A1, YELLOW_0:59;
then ~ x >= ~ y by YELLOW_7:1;
then (F opp+id) . i >= ~ y by YELLOW_9:7;
hence (F opp+id) . i >= (F opp+id) . j by YELLOW_9:7; :: thesis: verum