let S be antisymmetric with_suprema with_infima RelStr ; :: thesis: 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 ; :: thesis: ( [: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) ; :: according to WAYBEL_1:def 3 :: thesis: S is distributive
let x, y, z be Element of S; :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
consider t being Element of T;
t <= t ;
then A2: ( t "\/" t = t & t "/\" t = t ) by YELLOW_0:24, YELLOW_0:25;
thus x "/\" (y "\/" z) = [(x "/\" (y "\/" z)),t] `1 by MCART_1:7
.= ([x,t] "/\" [(y "\/" z),t]) `1 by A2, Th15
.= ([x,t] "/\" ([y,t] "\/" [z,t])) `1 by A2, Th16
.= (([x,t] "/\" [y,t]) "\/" ([x,t] "/\" [z,t])) `1 by A1
.= ([(x "/\" y),t] "\/" ([x,t] "/\" [z,t])) `1 by A2, Th15
.= ([(x "/\" y),t] "\/" [(x "/\" z),t]) `1 by A2, Th15
.= [((x "/\" y) "\/" (x "/\" z)),t] `1 by A2, Th16
.= (x "/\" y) "\/" (x "/\" z) by MCART_1:7 ; :: thesis: verum