let a, b be ordinal number ; :: thesis: ( 1 in a & 1 in b implies a in a |^|^ b )
assume Z0: 1 in a ; :: thesis: ( not 1 in b or a in a |^|^ b )
assume 1 in b ; :: thesis: a in a |^|^ b
then succ 1 c= b by ORDINAL1:33;
then Z1: 2 c= b ;
0 in 1 by NAT_1:45;
then 0 in a by Z0, ORDINAL1:19;
then ( a |^|^ 1 in a |^|^ 2 & a |^|^ 2 c= a |^|^ b ) by Z0, Z1, Th5, Th7;
then a |^|^ 1 in a |^|^ b ;
hence a in a |^|^ b by Th3; :: thesis: verum