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

proof

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

end;

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