let S be non empty FinSequence; :: thesis: for T being non empty Subset of (rng S) ex x being set st

( x in T & ( for y being set st y in T holds

x .. S <= y .. S ) )

let T be non empty Subset of (rng S); :: thesis: ex x being set st

( x in T & ( for y being set st y in T holds

x .. S <= y .. S ) )

deffunc H_{1}( set ) -> Element of omega = $1 .. S;

consider m being Element of T such that

A1: for y being Element of T holds H_{1}(m) <= H_{1}(y)
from PRE_CIRC:sch 5();

take m ; :: thesis: ( m in T & ( for y being set st y in T holds

m .. S <= y .. S ) )

thus m in T ; :: thesis: for y being set st y in T holds

m .. S <= y .. S

let y be set ; :: thesis: ( y in T implies m .. S <= y .. S )

assume y in T ; :: thesis: m .. S <= y .. S

hence m .. S <= y .. S by A1; :: thesis: verum

( x in T & ( for y being set st y in T holds

x .. S <= y .. S ) )

let T be non empty Subset of (rng S); :: thesis: ex x being set st

( x in T & ( for y being set st y in T holds

x .. S <= y .. S ) )

deffunc H

consider m being Element of T such that

A1: for y being Element of T holds H

take m ; :: thesis: ( m in T & ( for y being set st y in T holds

m .. S <= y .. S ) )

thus m in T ; :: thesis: for y being set st y in T holds

m .. S <= y .. S

let y be set ; :: thesis: ( y in T implies m .. S <= y .. S )

assume y in T ; :: thesis: m .. S <= y .. S

hence m .. S <= y .. S by A1; :: thesis: verum