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
set t = the Element of T;
let x, y, z be Element of S; :: according to WAYBEL_1:def 3 :: thesis: 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) ; :: thesis: verum