let S be antisymmetric with_suprema with_infima RelStr ; for T being reflexive antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
S is distributive
let T be reflexive antisymmetric with_suprema with_infima RelStr ; ( [:S,T:] is distributive implies S is distributive )
assume A1:
for x, y, z being Element of [:S,T:] holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
; WAYBEL_1:def 3 S is distributive
set t = the Element of T;
let x, y, z be Element of S; WAYBEL_1:def 3 x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A2:
the Element of T "/\" the Element of T = the Element of T
by YELLOW_0:25;
the Element of T <= the Element of T
;
then A3:
the Element of T "\/" the Element of T = the Element of T
by YELLOW_0:24;
thus x "/\" (y "\/" z) =
[(x "/\" (y "\/" z)), the Element of T] `1
.=
([x, the Element of T] "/\" [(y "\/" z), the Element of T]) `1
by A2, Th15
.=
([x, the Element of T] "/\" ([y, the Element of T] "\/" [z, the Element of T])) `1
by A3, Th16
.=
(([x, the Element of T] "/\" [y, the Element of T]) "\/" ([x, the Element of T] "/\" [z, the Element of T])) `1
by A1
.=
([(x "/\" y), the Element of T] "\/" ([x, the Element of T] "/\" [z, the Element of T])) `1
by A2, Th15
.=
([(x "/\" y), the Element of T] "\/" [(x "/\" z), the Element of T]) `1
by A2, Th15
.=
[((x "/\" y) "\/" (x "/\" z)), the Element of T] `1
by A3, Th16
.=
(x "/\" y) "\/" (x "/\" z)
; verum