let A be non empty Poset; :: thesis: for a being Element of A holds
( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
let a be Element of A; :: thesis: ( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus ( a is_minimal_in the InternalRel of A implies for b being Element of A holds not b < a ) :: thesis: ( ( for b being Element of A holds not b < a ) implies a is_minimal_in the InternalRel of A )
proof
assume A2: a is_minimal_in the InternalRel of A ; :: thesis: for b being Element of A holds not b < a
let b be Element of A; :: thesis: not b < a
( a = b or not [b,a] in the InternalRel of A ) by A1, A2;
then ( a = b or not b <= a ) ;
hence not b < a ; :: thesis: verum
end;
assume A3: for b being Element of A holds not b < a ; :: thesis: a is_minimal_in the InternalRel of A
thus a in field the InternalRel of A by A1; :: according to ORDERS_1:def 13 :: thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or not [b1,a] in the InternalRel of A )
let y be set ; :: thesis: ( not y in field the InternalRel of A or y = a or not [y,a] in the InternalRel of A )
assume that
A4: y in field the InternalRel of A and
A5: y <> a and
A6: [y,a] in the InternalRel of A ; :: thesis: contradiction
reconsider b = y as Element of A by A4, ORDERS_1:15;
b <= a by A6;
then b < a by A5;
hence contradiction by A3; :: thesis: verum