let a, b, c, d be ordinal number ; :: 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 Z0: 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 Z0, Th15a; :: thesis: verum
end;
end;
end;
assume Z3: ( ( 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 Z3;
suppose ( a = c & b in d ) ; :: thesis: a -Veblen b in c -Veblen d
hence a -Veblen b in c -Veblen d by Th15a; :: thesis: verum
end;
suppose Z4: ( 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 Th11a;
hence a -Veblen b in c -Veblen d by Z4, Th15a; :: thesis: verum
end;
suppose Z5: ( 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 Th11a;
hence a -Veblen b in c -Veblen d by Z5, Th15a; :: thesis: verum
end;
end;