let R be Relation; for x being set holds
( x is_minimal_in R ~ iff x is_maximal_in R )
let x be set ; ( x is_minimal_in R ~ iff x is_maximal_in R )
A1:
field R = field (R ~)
by RELAT_1:21;
thus
( x is_minimal_in R ~ implies x is_maximal_in R )
( x is_maximal_in R implies x is_minimal_in R ~ )proof
assume that A2:
x in field (R ~)
and A3:
for
y being
set holds
( not
y in field (R ~) or not
y <> x or not
[y,x] in R ~ )
;
ORDERS_1:def 13 x is_maximal_in R
thus
x in field R
by A2, RELAT_1:21;
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 A4:
y in field R
and A5:
y <> x
;
not [x,y] in R
not
[y,x] in R ~
by A1, A3, A4, A5;
hence
not
[x,y] in R
by RELAT_1:def 7;
verum
end;
assume that
A6:
x in field R
and
A7:
for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
; ORDERS_1:def 12 x is_minimal_in R ~
thus
x in field (R ~)
by A6, RELAT_1:21; ORDERS_1:def 13 for y being set holds
( not y in field (R ~) or not y <> x or not [y,x] in R ~ )
let y be set ; ( not y in field (R ~) or not y <> x or not [y,x] in R ~ )
assume that
A8:
y in field (R ~)
and
A9:
y <> x
; not [y,x] in R ~
not [x,y] in R
by A1, A7, A8, A9;
hence
not [y,x] in R ~
by RELAT_1:def 7; verum