theorem :: ORDINAL6:73

for a, b, c, d being Ordinal holds
( a -Veblen b in c -Veblen d iff ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) )