let R be Relation; for x being set st x is_superior_of R & R is antisymmetric holds
x is_maximal_in R
let x be set ; ( 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
; x is_maximal_in R
A3:
R is_antisymmetric_in field R
by A2;
thus A4:
x in field R
by A1; ORDERS_1:def 12 for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
let y be set ; ( 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
; contradiction
[y,x] in R
by A1, A5, A6;
hence
contradiction
by A4, A5, A6, A7, A3; verum