let a be Ordinal; :: thesis:
defpred S₁[ Ordinal] means 1 |^|^ $1 = 1;
A1: S₁[ 0 ] by Th13;
A2: for a being Ordinal st S₁[a] holds
S₁[ succ a]

end;

A3: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

let A be Ordinal; :: thesis:
assume that
A4: ( A <> 0 & A is limit_ordinal ) and
A5: for B being Ordinal st B in A holds
1 |^|^ B = 1 ; :: thesis:
deffunc H₁( Ordinal) -> Ordinal = 1 |^|^ $1;
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H₁(B) ) ) from ORDINAL2:sch 3();
A7: 1 |^|^ A = lim fi by A4, A6, Th15;
A8: rng fi c= {1}

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng fi ; :: thesis:
then consider y being object such that
A9: ( y in dom fi & x = fi . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by A9;
x = 1 |^|^ y by A6, A9
.= 1 by A5, A6, A9 ;
hence x in {1} by TARSKI:def 1; :: thesis:

end;

thus {} <> 1 ; :: thesis:
let b, c be Ordinal; :: thesis:
assume A10: ( b in 1 & 1 in c ) ; :: thesis:
set x = the Element of A;
reconsider x = the Element of A as Ordinal ;
take D = x; :: thesis:
thus D in dom fi by A4, A6; :: thesis:
let E be Ordinal; :: thesis:
assume ( D c= E & E in dom fi ) ; :: thesis:
then fi . E in rng fi by FUNCT_1:def 3;
hence ( b in fi . E & fi . E in c ) by A8, A10, TARSKI:def 1; :: thesis:

end;

end;