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