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₁( set ) -> Element of omega = $1 .. S;
consider m being Element of T such that
A1: for y being Element of T holds H₁(m) <= H₁(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