let p1, p2 be Element of P; :: thesis: ( p1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p1 <= p ) & p2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p2 <= p ) implies p1 = p2 )
assume ( p1 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p1 <= p ) & p2 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
p2 <= p ) ) ; :: thesis: p1 = p2
then ( p1 <= p2 & p2 <= p1 ) ;
hence p1 = p2 by ORDERS_2:2; :: thesis: verum