let X be ConstructorDB ; :: thesis: for x, y being Element of X holds

( x in y ref iff y in x occur )

let x, y be Element of X; :: thesis: ( x in y ref iff y in x occur )

then [x,y] in (@ the ref-operation of X) ~ by RELAT_1:169;

then [y,x] in @ the ref-operation of X by RELAT_1:def 7;

hence x in y ref by RELAT_1:169; :: thesis: verum

( x in y ref iff y in x occur )

let x, y be Element of X; :: thesis: ( x in y ref iff y in x occur )

hereby :: thesis: ( y in x occur implies x in y ref )

assume
y in x occur
; :: thesis: x in y ref assume
x in y ref
; :: thesis: y in x occur

then [y,x] in @ the ref-operation of X by RELAT_1:169;

then [x,y] in (@ the ref-operation of X) ~ by RELAT_1:def 7;

hence y in x occur by RELAT_1:169; :: thesis: verum

end;then [y,x] in @ the ref-operation of X by RELAT_1:169;

then [x,y] in (@ the ref-operation of X) ~ by RELAT_1:def 7;

hence y in x occur by RELAT_1:169; :: thesis: verum

then [x,y] in (@ the ref-operation of X) ~ by RELAT_1:169;

then [y,x] in @ the ref-operation of X by RELAT_1:def 7;

hence x in y ref by RELAT_1:169; :: thesis: verum