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 consider z being Element of L such that
A1: ( a = z & [y,z] in AR ) ;
thus [y,a] in AR by A1; :: thesis: verum

end;

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

proof

take x' ; :: thesis: ( a = x' & [y,x'] in AR )
thus ( a = x' & [y,x'] in AR ) by A2; :: 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