let S be non empty complete continuous Poset; :: thesis: for A being set st A is_FreeGen_set_of S holds
A is Subset of S
let A be set ; :: thesis: ( A is_FreeGen_set_of S implies A is Subset of S )
assume A1: A is_FreeGen_set_of S ; :: thesis: A is Subset of S
consider T being non empty complete continuous Poset;
consider f being Function of A,the carrier of T;
consider h being CLHomomorphism of S,T such that
A2: h | A = f and
for h' being CLHomomorphism of S,T st h' | A = f holds
h' = h by A1, Def1;
dom (h | A) = (dom h) /\ A by RELAT_1:90;
hence A is Subset of S by A2, FUNCT_2:def 1; :: thesis: verum