let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for T being InsType of (Trivial-AMI IL,N) holds AddressParts T = {0 }
let IL be non empty set ; :: thesis: for T being InsType of (Trivial-AMI IL,N) holds AddressParts T = {0 }
let T be InsType of (Trivial-AMI IL,N); :: thesis: AddressParts T = {0 }
set A = { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T } ;
{0 } = { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T } c= {0 }

let a be set ; :: thesis: ( a in {0 } implies a in { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T } )
assume a in {0 } ; :: thesis: a in { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T }
then A1: a = 0 by TARSKI:def 1;
A2: the Instructions of (Trivial-AMI IL,N) = {[0 ,{} ]} by AMI_1:def 2;
then InsCodes (Trivial-AMI IL,N) = {0 } by RELAT_1:23;
then A3: T = 0 by TARSKI:def 1;
reconsider I = [0 ,0 ] as Instruction of (Trivial-AMI IL,N) by A2, TARSKI:def 1;
A4: AddressPart I = 0 by Lm3;
InsCode I = 0 by MCART_1:def 1;
hence a in { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T } by A1, A3, A4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T } or a in {0 } )
assume a in { (AddressPart I) where I is Instruction of (Trivial-AMI IL,N) : InsCode I = T } ; :: thesis: a in {0 }
then ex I being Instruction of (Trivial-AMI IL,N) st
( a = AddressPart I & InsCode I = T ) ;
then a = 0 by Lm3;
hence a in {0 } by TARSKI:def 1; :: thesis: verum

end;

hence AddressParts T = {0 } ; :: thesis: verum