let L be RelStr ; :: thesis:
let X be set ; :: thesis:
let x be Element of L; :: thesis:

hereby :: thesis:

assume x is_maximal_in X ; :: thesis:
then A1: x is_maximal_wrt X, the InternalRel of L ;
hence x in X ; :: thesis:
let y be Element of L; :: thesis:

per cases by A1;

suppose not y in X ; :: thesis:

hence ( not y in X or not x < y ) ; :: thesis:

end;

suppose y = x ; :: thesis:

hence ( not y in X or not x < y ) ; :: thesis:

end;

suppose not [x,y] in the InternalRel of L ; :: thesis:

then not x <= y by ORDERS_2:def 5;
hence ( not y in X or not x < y ) by ORDERS_2:def 6; :: thesis:

end;

end;

end;

assume that
A2: x in X and
A3: for y being Element of L holds
( not y in X or not x < y ) ; :: thesis:
assume not x is_maximal_in X ; :: thesis:
then not x is_maximal_wrt X, the InternalRel of L ;
then consider y being set such that
A4: y in X and
A5: y <> x and
A6: [x,y] in the InternalRel of L by A2;
reconsider y = y as Element of L by A6, ZFMISC_1:87;
x <= y by A6, ORDERS_2:def 5;
then x < y by A5, ORDERS_2:def 6;
hence contradiction by A3, A4; :: thesis: