let A be non empty Poset; :: thesis: for a being Element of A holds
( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
let a be Element of A; :: thesis: ( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus ( a is_maximal_in the InternalRel of A implies for b being Element of A holds not a < b ) :: thesis: ( ( for b being Element of A holds not a < b ) implies a is_maximal_in the InternalRel of A )

proof

assume A2: a is_maximal_in the InternalRel of A ; :: thesis: for b being Element of A holds not a < b
let b be Element of A; :: thesis: not a < b
( a = b or not [a,b] in the InternalRel of A ) by A1, A2;
then ( a = b or not a <= b ) ;
hence not a < b ; :: thesis: verum

end;

assume A3: for b being Element of A holds not a < b ; :: thesis: a is_maximal_in the InternalRel of A
thus a in field the InternalRel of A by A1; :: according to ORDERS_1:def 12 :: thesis: for b₁ being set holds
( not b₁ in field the InternalRel of A or b₁ = a or not [a,b₁] in the InternalRel of A )
let y be set ; :: thesis: ( not y in field the InternalRel of A or y = a or not [a,y] in the InternalRel of A )
assume that
A4: y in field the InternalRel of A and
A5: y <> a and
A6: [a,y] in the InternalRel of A ; :: thesis: contradiction
reconsider b = y as Element of A by A4, ORDERS_1:15;
a <= b by A6;
then a < b by A5;
hence contradiction by A3; :: thesis: verum