let L be Lattice; :: thesis: for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let P be non empty ClosedSubset of L; :: thesis: for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p, q be Element of L; :: thesis: for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p9, q9 be Element of (latt (L,P)); :: thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 [= q9 ) )
assume A1: ( p = p9 & q = q9 ) ; :: thesis: ( p [= q iff p9 [= q9 )
thus ( p [= q implies p9 [= q9 ) :: thesis: ( p9 [= q9 implies p [= q )

proof

assume p "\/" q = q ; :: according to LATTICES:def 3 :: thesis: p9 [= q9
hence p9 "\/" q9 = q9 by A1, Th74; :: according to LATTICES:def 3 :: thesis: verum

end;

assume p9 "\/" q9 = q9 ; :: according to LATTICES:def 3 :: thesis: p [= q
hence p "\/" q = q by A1, Th74; :: according to LATTICES:def 3 :: thesis: verum