take {[0,{},{}]} ; :: thesis: ( not {[0,{},{}]} is empty & {[0,{},{}]} is standard-ins )
thus ( not {[0,{},{}]} is empty & {[0,{},{}]} is standard-ins ) ; :: thesis: verum