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