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

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