let X be set ; :: thesis: for L being complete continuous LATTICE
for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
A1: ( FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X)) & card X = card (FixedUltraFilters X) ) by Th10, Th16;
let L be complete continuous LATTICE; :: thesis: for G being set st G is_FreeGen_set_of L & card G = card X holds
L, InclPoset (Filt (BoolePoset X)) are_isomorphic
let G be set ; :: thesis: ( G is_FreeGen_set_of L & card G = card X implies L, InclPoset (Filt (BoolePoset X)) are_isomorphic )
assume ( G is_FreeGen_set_of L & card G = card X ) ; :: thesis: L, InclPoset (Filt (BoolePoset X)) are_isomorphic
hence L, InclPoset (Filt (BoolePoset X)) are_isomorphic by A1, Th17; :: thesis: verum