let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I)
let A be non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of 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

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

suppose not o in Out_U_Inp I ; :: thesis: o in Output I

hence o in Output I by A1; :: thesis: verum

end;

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

Out_\_Inp I c= Output I by Th10;
hence o in Output I by A3; :: thesis: verum

end;

end;

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:7; :: 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 Th11, XBOOLE_1:36;
hence (Output I) \/ (Input I) c= Out_U_Inp I by XBOOLE_1:8; :: thesis: verum