now :: thesis: for x being object st x in EvenNAT /\ {1,2} holds
x in {2}

let x be object ; :: thesis: ( x in EvenNAT /\ {1,2} implies b₁ in {2} )
assume A1: x in EvenNAT /\ {1,2} ; :: thesis: b₁ in {2}
then A2: x in EvenNAT by XBOOLE_0:def 4;
A3: x in {1,2} by A1, XBOOLE_0:def 4;

per cases ( x = 1 or x = 2 * 1 ) by A3, TARSKI:def 2;

suppose x = 1 ; :: thesis: b₁ in {2}

then x = 0 + 1 ;
then A4: x = (2 * 0) + 1 ;
ex k being Nat st x = 2 * k by A2;
hence x in {2} by A4; :: thesis: verum

end;

suppose x = 2 * 1 ; :: thesis: b₁ in {2}

hence x in {2} by TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A5: EvenNAT /\ {1,2} c= {2} ;
set q = {[2,(FIB . 2)]};
reconsider q = {[2,(FIB . 2)]} as FinSubsequence by Th17;
2 in NAT ;
then A6: 2 in dom FIB by FUNCT_2:def 1;

now :: thesis: for x being object st x in {2} holds
x in EvenNAT /\ {1,2}

let x be object ; :: thesis: ( x in {2} implies x in EvenNAT /\ {1,2} )
assume x in {2} ; :: thesis: x in EvenNAT /\ {1,2}
then x = 2 * 1 by TARSKI:def 1;
then ( x in EvenNAT & x in {1,2} ) by TARSKI:def 2;
hence x in EvenNAT /\ {1,2} by XBOOLE_0:def 4; :: thesis: verum

end;

then {2} c= EvenNAT /\ {1,2} ;
then EvenNAT /\ {1,2} = {2} by A5;
then EvenFibs 2 = Seq q by A6, FINSEQ_1:2, GRFUNC_1:28
.= <*(FIB . 2)*> by FINSEQ_3:157
.= <*1*> by Def2, Th21 ;
hence EvenFibs 2 = <*1*> ; :: thesis: verum