let N be with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of NAT ,N
for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)
let A be non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of NAT ,N; :: thesis: for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)
let I be Instruction of A; :: thesis: Out_\_Inp I = (Output I) \ (Input I)
for o being Object of A holds
( o in Out_\_Inp I iff o in (Output I) \ (Input I) )

proof

let o be Object of A; :: thesis: ( o in Out_\_Inp I iff o in (Output I) \ (Input I) )

hereby :: thesis: ( o in (Output I) \ (Input I) implies o in Out_\_Inp I )

assume A1: o in Out_\_Inp I ; :: thesis: o in (Output I) \ (Input I)
A2: Out_\_Inp I c= Output I by Th10;
Out_\_Inp I misses Input I by XBOOLE_1:85;
then not o in Input I by A1, XBOOLE_0:3;
hence o in (Output I) \ (Input I) by A1, A2, XBOOLE_0:def 5; :: thesis: verum

end;

assume A3: o in (Output I) \ (Input I) ; :: thesis: o in Out_\_Inp I
then A4: not o in Input I by XBOOLE_0:def 5;

per cases ( not o in Out_U_Inp I or o in Out_\_Inp I ) by A4, XBOOLE_0:def 5;

suppose A5: not o in Out_U_Inp I ; :: thesis: o in Out_\_Inp I

Output I c= Out_U_Inp I by Th11;
then not o in Output I by A5;
hence o in Out_\_Inp I by A3, XBOOLE_0:def 5; :: thesis: verum

end;

suppose o in Out_\_Inp I ; :: thesis: o in Out_\_Inp I

hence o in Out_\_Inp I ; :: thesis: verum

end;

end;

end;

hence Out_\_Inp I = (Output I) \ (Input I) by SUBSET_1:8; :: thesis: verum