let x, y be Element of (ClOpers L); :: according to WAYBEL_1:def 1 :: thesis: ( not (ClImageMap L) . x = (ClImageMap L) . y or x = y )
reconsider a = x, b = y as closure Function of L,L by Th10;
set f = ClImageMap L;
assume (ClImageMap L) . x = (ClImageMap L) . y ; :: thesis: x = y
then Image a = (ClImageMap L) . y by Def4
.= Image b by Def4 ;
hence x = closure_op (Image b) by Th19
.= y by Th19 ;
:: thesis: verum