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

proof

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

end;

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