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