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
set s = the Element of S;
let x, y, z be Element of T; :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A2: the Element of S "/\" the Element of S = the Element of S by YELLOW_0:25;
the Element of S <= the Element of S ;
then A3: the Element of S "\/" the Element of S = the Element of S by YELLOW_0:24;
thus x "/\" (y "\/" z) = [ the Element of S,(x "/\" (y "\/" z))] `2
.= ([ the Element of S,x] "/\" [ the Element of S,(y "\/" z)]) `2 by A2, Th15
.= ([ the Element of S,x] "/\" ([ the Element of S,y] "\/" [ the Element of S,z])) `2 by A3, Th16
.= (([ the Element of S,x] "/\" [ the Element of S,y]) "\/" ([ the Element of S,x] "/\" [ the Element of S,z])) `2 by A1
.= ([ the Element of S,(x "/\" y)] "\/" ([ the Element of S,x] "/\" [ the Element of S,z])) `2 by A2, Th15
.= ([ the Element of S,(x "/\" y)] "\/" [ the Element of S,(x "/\" z)]) `2 by A2, Th15
.= [ the Element of S,((x "/\" y) "\/" (x "/\" z))] `2 by A3, Th16
.= (x "/\" y) "\/" (x "/\" z) ; :: thesis: verum