( not MultiGraphStruct(# {0},{0},op1,op1 #) is empty & not MultiGraphStruct(# {0},{0},op1,op1 #) is void ) ;
hence ex b₁ being MultiGraphStruct st
( b₁ is strict & not b₁ is empty & not b₁ is void ) ; :: thesis: verum