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 and
A3: for r being Element of L st X is_less_than r holds
p1 [= r and
A4: X is_less_than p2 and
A5: for r being Element of L st X is_less_than r holds
p2 [= r ; :: thesis: p1 = p2
A6: p1 [= p2 by A3, A4;
p2 [= p1 by A2, A5;
hence p1 = p2 by A1, A6, LATTICES:8; :: thesis: verum