let R be Ring; :: thesis: for i1 being Nat holds JUMP (goto (i1,R)) = {i1}
let i1 be Nat; :: thesis: JUMP (goto (i1,R)) = {i1}
set X = { (NIC ((goto (i1,R)),il)) where il is Nat : verum } ;
now :: thesis: for x being object holds
( ( x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum } ) )
let x be object ; :: thesis: ( ( x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum } ) )
hereby :: thesis: ( x in {i1} implies x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum } )
reconsider il1 = 1 as Element of NAT ;
A1: NIC ((goto (i1,R)),il1) in { (NIC ((goto (i1,R)),il)) where il is Nat : verum } ;
assume x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum } ; :: thesis: x in {i1}
then x in NIC ((goto (i1,R)),il1) by A1, SETFAM_1:def 1;
hence x in {i1} by Th29; :: thesis: verum
end;
assume x in {i1} ; :: thesis: x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum }
then A2: x = i1 by TARSKI:def 1;
A3: now :: thesis: for Y being set st Y in { (NIC ((goto (i1,R)),il)) where il is Nat : verum } holds
i1 in Y
let Y be set ; :: thesis: ( Y in { (NIC ((goto (i1,R)),il)) where il is Nat : verum } implies i1 in Y )
assume Y in { (NIC ((goto (i1,R)),il)) where il is Nat : verum } ; :: thesis: i1 in Y
then consider il being Nat such that
A4: Y = NIC ((goto (i1,R)),il) ;
NIC ((goto (i1,R)),il) = {i1} by Th29;
hence i1 in Y by A4, TARSKI:def 1; :: thesis: verum
end;
NIC ((goto (i1,R)),i1) in { (NIC ((goto (i1,R)),il)) where il is Nat : verum } ;
hence x in meet { (NIC ((goto (i1,R)),il)) where il is Nat : verum } by A2, A3, SETFAM_1:def 1; :: thesis: verum
end;
hence JUMP (goto (i1,R)) = {i1} by TARSKI:2; :: thesis: verum