let a, b be Ordinal; :: thesis: ( 1 in a & 1 in b implies a in a |^|^ b )
assume A1: 1 in a ; :: thesis: ( not 1 in b or a in a |^|^ b )
assume 1 in b ; :: thesis: a in a |^|^ b
then A2: succ 1 c= b by ORDINAL1:21;
0 in Segm 1 by NAT_1:44;
then 0 in a by A1, ORDINAL1:10;
then ( a |^|^ 1 in a |^|^ 2 & a |^|^ 2 c= a |^|^ b ) by A1, A2, Th21, Th24;
then a |^|^ 1 in a |^|^ b ;
hence a in a |^|^ b by Th16; :: thesis: verum