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 )
thus ( a in downarrow y implies [a,y] in the InternalRel of L ) by ORDERS_2:def 5, WAYBEL_0:17; :: thesis: ( [a,y] in the InternalRel of L implies a in downarrow y )
assume A1: [a,y] in the InternalRel of L ; :: thesis: a in downarrow y
then reconsider a9 = a as Element of L by ZFMISC_1:87;
a9 <= y by A1, ORDERS_2:def 5;
hence a in downarrow y by WAYBEL_0:17; :: thesis: verum