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:5; :: 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 & Z [= X ) and
A2: for V being Element of L st Y [= V & Z [= V holds
X [= V ; :: thesis: X = Y "\/" Z
A3: Y "\/" Z [= X by A1, FILTER_0:6;
( Y [= Y "\/" Z & Z [= Y "\/" Z ) by LATTICES:5;
then X [= Y "\/" Z by A2;
hence X = Y "\/" Z by A3; :: thesis: verum