let A be Ordinal; :: thesis: ( A <> {} implies exp {} ,A = {} )
defpred S₁[ Ordinal] means ( $1 <> {} implies exp {} ,$1 = {} );
A1: S₁[ {} ] ;
A2: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume ( S₁[B] & succ B <> {} ) ; :: thesis: exp {} ,(succ B) = {}
thus exp {} ,(succ B) = {} *^ (exp {} ,B) by ORDINAL2:61
.= {} by ORDINAL2:52 ; :: thesis: verum

end;

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

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for C being Ordinal st C in A holds
S₁[C] ) implies S₁[A] )
assume that
A4: ( A <> {} & A is limit_ordinal ) and
A5: for C being Ordinal st C in A holds
S₁[C] and
A <> {} ; :: thesis: exp {} ,A = {}
deffunc H₁( Ordinal) -> set = exp {} ,$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();
{} is_limes_of fi

proof

per cases ( {} = {} or {} <> {} ) ;
:: according to ORDINAL2:def 13

case {} = {} ; :: thesis: ex b₁ being set st
( b₁ in dom fi & ( for b₂ being set holds
( not b₁ c= b₂ or not b₂ in dom fi or fi . b₂ = {} ) ) )

take B = 1; :: thesis: ( B in dom fi & ( for b₁ being set holds
( not B c= b₁ or not b₁ in dom fi or fi . b₁ = {} ) ) )
{} in A by A4, ORDINAL3:10;
hence B in dom fi by A4, A6, Lm3, ORDINAL1:41; :: thesis: for b₁ being set holds
( not B c= b₁ or not b₁ in dom fi or fi . b₁ = {} )
let D be Ordinal; :: thesis: ( not B c= D or not D in dom fi or fi . D = {} )
assume A7: B c= D ; :: thesis: ( not D in dom fi or fi . D = {} )
assume D in dom fi ; :: thesis: fi . D = {}
then ( S₁[D] & fi . D = exp {} ,D ) by A5, A6;
hence fi . D = {} by A7, Lm3, ORDINAL1:33; :: thesis: verum

end;

case {} <> {} ; :: thesis: for b₁, b₂ being set holds
( not b₁ in {} or not {} in b₂ or ex b₃ being set st
( b₃ in dom fi & ( for b₄ being set holds
( not b₃ c= b₄ or not b₄ in dom fi or ( b₁ in fi . b₄ & fi . b₄ in b₂ ) ) ) ) )

thus for b₁, b₂ being set holds
( not b₁ in {} or not {} in b₂ or ex b₃ being set st
( b₃ in dom fi & ( for b₄ being set holds
( not b₃ c= b₄ or not b₄ in dom fi or ( b₁ in fi . b₄ & fi . b₄ in b₂ ) ) ) ) ) ; :: thesis: verum

end;

end;

end;

then ( lim fi = {} & exp {} ,A = lim fi ) by A4, A6, ORDINAL2:62, ORDINAL2:def 14;
hence exp {} ,A = {} ; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A1, A2, A3);
hence ( A <> {} implies exp {} ,A = {} ) ; :: thesis: verum