let L be non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ; :: thesis: ( L is degenerated implies L is trivial )
assume A1: 0. L = 1. L ; :: according to STRUCT_0:def 8 :: thesis: L is trivial
let u be Element of L; :: according to STRUCT_0:def 18 :: thesis: u = 0. L
thus u = u * (1. L)
.= 0. L by A1 ; :: thesis: verum