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

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