A1: ( not MultiGraphStruct(# 1,1,op1 ,op1 #) is empty & not MultiGraphStruct(# 1,1,op1 ,op1 #) is void ) ;
thus ex b₁ being MultiGraphStruct st
( b₁ is strict & not b₁ is empty & not b₁ is void ) by A1; :: thesis: verum