let I be set ; :: thesis: for R being non empty transitive asymmetric RelStr
for x being Element of R st x in I & ( for y being Element of R st y in I & y <> x holds
x ## y ) holds
x is_maximal_in I
let R be non empty transitive asymmetric RelStr ; :: thesis: for x being Element of R st x in I & ( for y being Element of R st y in I & y <> x holds
x ## y ) holds
x is_maximal_in I
let x be Element of R; :: thesis: ( x in I & ( for y being Element of R st y in I & y <> x holds
x ## y ) implies x is_maximal_in I )
assume Z0: x in I ; :: thesis: ( ex y being Element of R st
( y in I & y <> x & not x ## y ) or x is_maximal_in I )
assume Z1: for y being Element of R st y in I & y <> x holds
x ## y ; :: thesis: x is_maximal_in I
for y being Element of R holds
( not y in I or not x < y )

proof

let y be Element of R; :: thesis: ( not y in I or not x < y )
assume ( y in I & x <= y & x <> y ) ; :: according to ORDERS_2:def 6 :: thesis: contradiction
then ( x ## y & x <= y ) by Z1;
hence contradiction ; :: thesis: verum

end;

hence x is_maximal_in I by Z0, WAYBEL_4:55; :: thesis: verum