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