let R be Relation; :: thesis: for x being set st x is_superior_of R & R is antisymmetric holds
x is_maximal_in R
let x be set ; :: thesis: ( x is_superior_of R & R is antisymmetric implies x is_maximal_in R )
assume that
A1: x is_superior_of R and
A2: R is antisymmetric ; :: thesis: x is_maximal_in R
A3: R is_antisymmetric_in field R by A2, RELAT_2:def 12;
thus A4: x in field R by A1, Def13; :: according to ORDERS_1:def 11 :: thesis: for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
let y be set ; :: thesis: ( not y in field R or not y <> x or not [x,y] in R )
assume that
A5: y in field R and
A6: y <> x and
A7: [x,y] in R ; :: thesis: contradiction
[y,x] in R by A1, A5, A6, Def13;
hence contradiction by A4, A5, A6, A7, A3, RELAT_2:def 4; :: thesis: verum