let R be non empty transitive antisymmetric with_finite_clique# RelStr ; :: thesis: for x being Element of R ex y being Element of R st
( y is_maximal_in [#] R & ( y = x or x < y ) )
let x be Element of R; :: thesis: ex y being Element of R st
( y is_maximal_in [#] R & ( y = x or x < y ) )
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 object such that
A1: y in maximals sU by XBOOLE_0:def 1;
reconsider y = y as Element of sU by A1;
A2: [#] sU = Upper {x} by YELLOW_0:def 15;
then A3: y is_maximal_in Upper {x} by A1, Def10;
reconsider y9 = y as Element of R by YELLOW_0:58;
take y9 ; :: thesis: ( y9 is_maximal_in [#] R & ( y9 = x or x < y9 ) )
Upper {x} c= the carrier of sU by YELLOW_0:def 15;
hence y9 is_maximal_in [#] R by A3, Th32, Th25; :: thesis: ( y9 = x or x < y9 )

per cases ( y9 = x or y9 <> x ) ;

suppose y9 = x ; :: thesis: ( y9 = x or x < y9 )

hence ( y9 = x or x < y9 ) ; :: thesis: verum

end;

suppose y9 <> x ; :: thesis: ( y9 = x or x < y9 )

then not y9 in {x} by TARSKI:def 1;
then y9 in uparrow x by A2, XBOOLE_0:def 3;
then x <= y9 by WAYBEL_0:18;
hence ( y9 = x or x < y9 ) ; :: thesis: verum

end;

end;