let L be non empty RelStr ; :: thesis: for AR being Relation of L
for a being object
for y being Element of L holds
( a in AR -below y iff [a,y] in AR )
let AR be Relation of L; :: thesis: for a being object
for y being Element of L holds
( a in AR -below y iff [a,y] in AR )
let a be object ; :: thesis: for y being Element of L holds
( a in AR -below y iff [a,y] in AR )
let y be Element of L; :: thesis: ( a in AR -below y iff [a,y] in AR )
( a in AR -below y iff [a,y] in AR )

proof

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

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

end;

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

proof

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

end;

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

end;

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