let R be non empty transitive antisymmetric with_finite_clique# RelStr ; :: thesis: for x being Element of ex y being Element of st
( y is_maximal_in [#] R & ( y = x or x < y ) )
let x be Element of ; :: thesis: ex y being Element of st
( y is_maximal_in [#] R & ( y = x or x < y ) )
set cR = the carrier of R;
set ax = Upper {x};
set sU = subrelstr (Upper {x});
reconsider sU = subrelstr (Upper {x}) as non empty transitive antisymmetric with_finite_clique# RelStr ;
consider y being set such that
A: y in maximals sU by XBOOLE_0:def 1;
reconsider y = y as Element of by A;
C: [#] sU = Upper {x} by YELLOW_0:def 15;
B: y is_maximal_in Upper {x} by A, C, Lmax;
reconsider y' = y as Element of by YELLOW_0:59;
take y' ; :: thesis: ( y' is_maximal_in [#] R & ( y' = x or x < y' ) )
Upper {x} c= the carrier of sU by YELLOW_0:def 15;
hence y' is_maximal_in [#] R by B, SPmax, Pmaxmax; :: thesis: ( y' = x or x < y' )

per cases ( y' = x or y' <> x ) ;

suppose y' = x ; :: thesis: ( y' = x or x < y' )

hence ( y' = x or x < y' ) ; :: thesis: verum

end;

suppose y' <> x ; :: thesis: ( y' = x or x < y' )

then not y' in {x} by TARSKI:def 1;
then y' in uparrow x by XBOOLE_0:def 3, C;
then x <= y' by WAYBEL_0:18;
hence ( y' = x or x < y' ) by ORDERS_2:def 10; :: thesis: verum

end;

end;