let L be 1 -element reflexive RelStr ; :: thesis: ( L is distributive & L is complemented )
thus L is distributive :: thesis: L is complemented

proof

let x, y, z be Element of L; :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by STRUCT_0:def 10; :: thesis: verum

end;

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