let L be complete LATTICE; :: thesis: DsupClOpers L,(Subalgebras L) opp are_isomorphic
set f = (ClImageMap L) | (DsupClOpers L);
A1: Image ((ClImageMap L) | (DsupClOpers L)) = (Subalgebras L) opp by Th29;
then reconsider g = corestr ((ClImageMap L) | (DsupClOpers L)) as Function of (DsupClOpers L),((Subalgebras L) opp ) ;
take g ; :: according to WAYBEL_1:def 8 :: thesis: g is isomorphic
thus g is isomorphic by A1; :: thesis: verum