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_U_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_U_Inp I = (Output I) \/ (Input I)
let I be Instruction of A; :: thesis: Out_U_Inp I = (Output I) \/ (Input I)
for o being Object of A st o in Out_U_Inp I holds
o in (Output I) \/ (Input I)
proof
let o be Object of A; :: thesis: ( o in Out_U_Inp I implies o in (Output I) \/ (Input I) )
assume A1: o in Out_U_Inp I ; :: thesis: o in (Output I) \/ (Input I)
( o in Input I or o in Output I )
proof
assume A2: not o in Input I ; :: thesis: o in Output I
end;
hence o in (Output I) \/ (Input I) by XBOOLE_0:def 3; :: thesis: verum
end;
hence Out_U_Inp I c= (Output I) \/ (Input I) by SUBSET_1:2; :: according to XBOOLE_0:def 10 :: thesis: (Output I) \/ (Input I) c= Out_U_Inp I
( Output I c= Out_U_Inp I & Input I c= Out_U_Inp I ) by Th4, XBOOLE_1:36;
hence (Output I) \/ (Input I) c= Out_U_Inp I by XBOOLE_1:8; :: thesis: verum