let S be complete LATTICE; :: thesis: UPS (S,(BoolePoset {0})), InclPoset (sigma S) are_isomorphic
consider F being Function of (UPS (S,(BoolePoset {0}))),(InclPoset (sigma S)) such that
A1: F is isomorphic and
for f being directed-sups-preserving Function of S,(BoolePoset {0}) holds F . f = f " {1} by Th33;
take F ; :: according to WAYBEL_1:def 8 :: thesis: F is isomorphic
thus F is isomorphic by A1; :: thesis: verum