let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic
let B be with_bottom CLbasis of L; :: thesis: CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic
deffunc H₁( Element of (subrelstr B)) -> Element of K32( the carrier of (subrelstr B)) = downarrow $1;
A1: for x being Element of (subrelstr B) holds H₁(x) is Element of (CompactSublatt (InclPoset (Ids (subrelstr B))))

proof

let x be Element of (subrelstr B); :: thesis: H₁(x) is Element of (CompactSublatt (InclPoset (Ids (subrelstr B))))
downarrow x in { (downarrow b) where b is Element of (subrelstr B) : verum } ;
hence H₁(x) is Element of (CompactSublatt (InclPoset (Ids (subrelstr B)))) by Th68; :: thesis: verum

end;

consider f being Function of (subrelstr B),(CompactSublatt (InclPoset (Ids (subrelstr B)))) such that
A2: for x being Element of (subrelstr B) holds f . x = H₁(x) from FUNCT_2:sch 9(A1);
f is isomorphic by A2, WAYBEL13:13;
then subrelstr B, CompactSublatt (InclPoset (Ids (subrelstr B))) are_isomorphic by WAYBEL_1:def 8;
hence CompactSublatt (InclPoset (Ids (subrelstr B))), subrelstr B are_isomorphic by WAYBEL_1:6; :: thesis: verum