let R be Ring; :: thesis: for a being Data-Location of R
for i1 being Nat holds JUMP (a =0_goto i1) = {i1}
let a be Data-Location of R; :: thesis: for i1 being Nat holds JUMP (a =0_goto i1) = {i1}
let i1 be Nat; :: thesis: JUMP (a =0_goto i1) = {i1}
set X = { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ;

now :: thesis: for x being object holds
( ( x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ) )

let x be object ; :: thesis: ( ( x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } implies x in {i1} ) & ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ) )

A1: now :: thesis: for Y being set st Y in { (NIC ((a =0_goto i1),il)) where il is Nat : verum } holds
i1 in Y

let Y be set ; :: thesis: ( Y in { (NIC ((a =0_goto i1),il)) where il is Nat : verum } implies i1 in Y )
assume Y in { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ; :: thesis: i1 in Y
then ex il being Nat st Y = NIC ((a =0_goto i1),il) ;
hence i1 in Y by Th31; :: thesis: verum

end;

hereby :: thesis: ( x in {i1} implies x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } )

reconsider il1 = 1, il2 = 2 as Element of NAT ;
assume A2: x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ; :: thesis: x in {i1}
A3: NIC ((a =0_goto i1),il2) c= {i1,(il2 + 1)} by Th31;
NIC ((a =0_goto i1),il2) in { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ;
then x in NIC ((a =0_goto i1),il2) by A2, SETFAM_1:def 1;
then A4: ( x = i1 or x = il2 + 1 ) by A3, TARSKI:def 2;
A5: NIC ((a =0_goto i1),il1) c= {i1,(il1 + 1)} by Th31;
NIC ((a =0_goto i1),il1) in { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ;
then x in NIC ((a =0_goto i1),il1) by A2, SETFAM_1:def 1;
then ( x = i1 or x = il1 + 1 ) by A5, TARSKI:def 2;
hence x in {i1} by A4, TARSKI:def 1; :: thesis: verum

end;

assume x in {i1} ; :: thesis: x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum }
then A6: x = i1 by TARSKI:def 1;
NIC ((a =0_goto i1),i1) in { (NIC ((a =0_goto i1),il)) where il is Nat : verum } ;
hence x in meet { (NIC ((a =0_goto i1),il)) where il is Nat : verum } by A6, A1, SETFAM_1:def 1; :: thesis: verum

end;

hence JUMP (a =0_goto i1) = {i1} by TARSKI:2; :: thesis: verum