consider k being Nat such that A5:
S1[k]
and A6:
for n being Nat st S1[n] holds n <= k
fromNAT_1:sch 6(A1, A3);
for n being Element of NAT st S1[n] holds n <= k
byA6; hence
ex k being Element of NAT st ( S1[k] & ( for n being Element of NAT st S1[n] holds n <= k ) )
byA5; :: thesis: verum
end;
then consider k being Element of NAT such that A7:
( S1[k] & ( for n being Element of NAT st S1[n] holds n <= k ) )
; consider x being Element of L such that A8:
x in X
and A9:
( k =height x & ( for n being Element of NAT st ex y being Element of L st ( y in X & n =height y ) holds n <= k ) )
byA7;
for y being Element of L st y in X holds not x < y