let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N
for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)
let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over 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 )

A1: Out_\_Inp I c= Output I by Th3;
assume A2: o in Out_\_Inp I ; :: thesis: o in (Output I) \ (Input I)
Out_\_Inp I misses Input I by XBOOLE_1:85;
then not o in Input I by A2, XBOOLE_0:3;
hence o in (Output I) \ (Input I) by A2, A1, 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 Th4;
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:3; :: thesis: verum