let p1, p2 be Element of L; :: thesis: ( X is_less_than p1 & ( for r being Element of L st X is_less_than r holds
p1 [= r ) & X is_less_than p2 & ( for r being Element of L st X is_less_than r holds
p2 [= r ) implies p1 = p2 )
assume that
A2: ( X is_less_than p1 & ( for r being Element of L st X is_less_than r holds
p1 [= r ) ) and
A3: ( X is_less_than p2 & ( for r being Element of L st X is_less_than r holds
p2 [= r ) ) ; :: thesis: p1 = p2
( p1 [= p2 & p2 [= p1 ) by A2, A3;
hence p1 = p2 by A1, LATTICES:26; :: thesis: verum