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