let f be 3 -element natural-valued increasing positive FinSequence; :: thesis: ex a, b, c being positive Nat st
( f = <*a,b,c*> & a < b & b < c )
consider a, b, c being positive Nat such that
A1: f = <*a,b,c*> by Th47;
take a ; :: thesis: ex b, c being positive Nat st
( f = <*a,b,c*> & a < b & b < c )
take b ; :: thesis: ex c being positive Nat st
( f = <*a,b,c*> & a < b & b < c )
take c ; :: thesis: ( f = <*a,b,c*> & a < b & b < c )
thus f = <*a,b,c*> by A1; :: thesis: ( a < b & b < c )
A2: ( f . 1 = a & f . 2 = b & f . 3 = c ) by A1;
A3: dom f = {1,2,3} by A1, NOMIN_2:4;
( 1 in {1,2,3} & 2 in {1,2,3} & 3 in {1,2,3} ) by ENUMSET1:def 1;
hence ( a < b & b < c ) by A2, A3, VALUED_0:def 13; :: thesis: verum