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 )
hereby :: thesis: ( y in x occur implies 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;
assume y in x occur ; :: thesis: x in y ref
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