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 Th11;
set f = ClImageMap L;
assume (ClImageMap L) . x = (ClImageMap L) . y ; :: thesis: x = y
then Image a = (ClImageMap L) . y by Def5
.= Image b by Def5 ;
hence x = closure_op (Image b) by Th20
.= y by Th20 ;
:: thesis: verum