let x, y, z be Element of (InclPoset the topology of T); :: according to WAYBEL_1:def 3 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = x /\ (y "\/" z) by Th18
.= x /\ (y \/ z) by Th18
.= (x /\ y) \/ (x /\ z) by XBOOLE_1:23
.= (x "/\" y) \/ (x /\ z) by Th18
.= (x "/\" y) \/ (x "/\" z) by Th18
.= (x "/\" y) "\/" (x "/\" z) by Th18 ; :: thesis: verum