set T = the non empty complete continuous Poset;
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
set f = the Function of A, the carrier of the non empty complete continuous Poset;
consider h being CLHomomorphism of S, the non empty complete continuous Poset such that
A2: h | A = the Function of A, the carrier of the non empty complete continuous Poset and
for h9 being CLHomomorphism of S, the non empty complete continuous Poset st h9 | A = the Function of A, the carrier of the non empty complete continuous Poset holds
h9 = h by A1;
dom (h | A) = (dom h) /\ A by RELAT_1:61;
hence A is Subset of S by A2, FUNCT_2:def 1; :: thesis: verum