take T = TBAStruct(# {0},op1,op3 #); :: thesis: ( T is trivial & not T is empty )
thus ( T is trivial & not T is empty ) ; :: thesis: verum