let a be set ; :: thesis: for L being sup-Semilattice
for AR being Relation of L
for y being Element of L holds
( a in AR -above y iff [y,a] in AR )
let L be with_suprema Poset; :: thesis: for AR being Relation of L
for y being Element of L holds
( a in AR -above y iff [y,a] in AR )
let AR be Relation of L; :: thesis: for y being Element of L holds
( a in AR -above y iff [y,a] in AR )
let y be Element of L; :: thesis: ( a in AR -above y iff [y,a] in AR )
( a in AR -above y iff [y,a] in AR )

proof

hereby :: thesis: ( [y,a] in AR implies a in AR -above y )

assume a in AR -above y ; :: thesis: [y,a] in AR
then ex z being Element of L st
( a = z & [y,z] in AR ) ;
hence [y,a] in AR ; :: thesis: verum

end;

assume A1: [y,a] in AR ; :: thesis: a in AR -above y
then reconsider x9 = a as Element of L by ZFMISC_1:87;
ex z being Element of L st
( a = z & [y,z] in AR )

proof

take x9 ; :: thesis: ( a = x9 & [y,x9] in AR )
thus ( a = x9 & [y,x9] in AR ) by A1; :: thesis: verum

end;

hence a in AR -above y ; :: thesis: verum

end;

hence ( a in AR -above y iff [y,a] in AR ) ; :: thesis: verum