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