let L be 1 -element reflexive RelStr ; :: thesis: ( L is distributive & L is complemented )
thus L is distributive by STRUCT_0:def 10; :: thesis: L is complemented
let x be Element of L; :: according to WAYBEL_1:def 24 :: thesis: ex b₁ being Element of the carrier of L st b₁ is_a_complement_of x
take y = x; :: thesis: y is_a_complement_of x
thus x "\/" y = Top L by STRUCT_0:def 10; :: according to WAYBEL_1:def 23 :: thesis: x "/\" y = Bottom L
thus x "/\" y = Bottom L by STRUCT_0:def 10; :: thesis: verum