let a, b, c, d be Ordinal; :: thesis: ( 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 ) ) )
hereby :: thesis: ( ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) implies a -Veblen b in c -Veblen d )
assume A1: a -Veblen b in c -Veblen d ; :: thesis: ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) )
per cases ( a = c or a in c or c in a ) by ORDINAL1:14;
case a = c ; :: thesis: b in d
hence b in d by A1, Th72; :: thesis: verum
end;
end;
end;
assume A2: ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) ; :: thesis: a -Veblen b in c -Veblen d
per cases ( ( a = c & b in d ) or ( a in c & b in c -Veblen d ) or ( c in a & a -Veblen b in d ) ) by A2;
suppose ( a = c & b in d ) ; :: thesis: a -Veblen b in c -Veblen d
hence a -Veblen b in c -Veblen d by Th72; :: thesis: verum
end;
suppose A3: ( a in c & b in c -Veblen d ) ; :: thesis: a -Veblen b in c -Veblen d
then a -Veblen (c -Veblen d) = c -Veblen d by Th70;
hence a -Veblen b in c -Veblen d by A3, Th72; :: thesis: verum
end;
suppose A4: ( c in a & a -Veblen b in d ) ; :: thesis: a -Veblen b in c -Veblen d
then c -Veblen (a -Veblen b) = a -Veblen b by Th70;
hence a -Veblen b in c -Veblen d by A4, Th72; :: thesis: verum
end;
end;