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

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