let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty IC-Ins-separated AMI-Struct of N
for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Input I
let A be non empty IC-Ins-separated AMI-Struct of N; :: thesis: for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Input I
let I be Instruction of A; :: thesis: for o being Object of A st ObjectKind o is trivial holds
not o in Input I
let o be Object of A; :: thesis: ( ObjectKind o is trivial implies not o in Input I )
A1: Input I c= Out_U_Inp I by XBOOLE_1:36;
assume ObjectKind o is trivial ; :: thesis: not o in Input I
hence not o in Input I by A1, Th15; :: thesis: verum