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_{1} being Element of the carrier of L st b_{1} 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

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

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