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

proof

assume A2: a is_inferior_of the InternalRel of A ; :: thesis: for b being Element of A st a <> b holds
a < b
let b be Element of A; :: thesis: ( a <> b implies a < b )
assume A3: a <> b ; :: thesis: a < b
then [a,b] in the InternalRel of A by A1, A2;
then a <= b ;
hence a < b by A3; :: thesis: verum

end;

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