let L be lower-bounded with_suprema Poset; :: thesis: for AR being Relation of L
for a being set
for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
let AR be Relation of L; :: thesis: for a being set
for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
let a be set ; :: thesis: for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
let y be Element of L; :: thesis: ( a in downarrow y iff [a,y] in the InternalRel of L )

hereby :: thesis: ( [a,y] in the InternalRel of L implies a in downarrow y )

assume A1: a in downarrow y ; :: thesis: [a,y] in the InternalRel of L
then reconsider a9 = a as Element of L ;
a9 <= y by A1, WAYBEL_0:17;
hence [a,y] in the InternalRel of L by ORDERS_2:def 9; :: thesis: verum

end;

assume A2: [a,y] in the InternalRel of L ; :: thesis: a in downarrow y
then reconsider a9 = a as Element of L by ZFMISC_1:106;
a9 <= y by A2, ORDERS_2:def 9;
hence a in downarrow y by WAYBEL_0:17; :: thesis: verum