let L be 0_Lattice; :: thesis: for X, Y, Z being Element of L st X [= Y & X [= Z & Y misses Z holds
X = Bottom L
let X, Y, Z be Element of L; :: thesis: ( X [= Y & X [= Z & Y misses Z implies X = Bottom L )
assume that
A1: ( X [= Y & X [= Z ) and
A2: Y misses Z ; :: thesis: X = Bottom L
Y "/\" Z = Bottom L by A2, Def4;
hence X = Bottom L by A1, Th25, FILTER_0:7; :: thesis: verum