thus ( V is trivial implies for a being Element of V holds a = 0. V ) ; :: thesis: ( ( for u being Element of V holds u = 0. V ) implies V is trivial )
assume A1: for a being Element of V holds a = 0. V ; :: thesis: V is trivial
let a, b be Element of V; :: according to STRUCT_0:def 10 :: thesis: a = b
thus a = 0. V by A1
.= b by A1 ; :: thesis: verum