let L be Lattice; :: thesis: for X, Y, Z being Element of L holds
( X = Y "/\" Z iff ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) )
let X, Y, Z be Element of L; :: thesis: ( X = Y "/\" Z iff ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) )
thus ( X = Y "/\" Z implies ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) ) by FILTER_0:7, LATTICES:6; :: thesis: ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) implies X = Y "/\" Z )
assume that
A1: ( X [= Y & X [= Z ) and
A2: for V being Element of L st V [= Y & V [= Z holds
V [= X ; :: thesis: X = Y "/\" Z
A3: X [= Y "/\" Z by A1, FILTER_0:7;
( Y "/\" Z [= Y & Y "/\" Z [= Z ) by LATTICES:6;
then Y "/\" Z [= X by A2;
hence X = Y "/\" Z by A3; :: thesis: verum