let X be non empty set ; :: thesis: ( X is axiom_GU4 iff X is FamUnion-closed )

hereby :: thesis: ( X is FamUnion-closed implies X is axiom_GU4 )

assume A1: X is axiom_GU4 ; :: thesis: X is FamUnion-closed

now :: thesis: for A being set
for f being Function st dom f = A & rng f c= X & A in X holds
union (rng f) in X

let A be set ; :: thesis: for f being Function st dom f = A & rng f c= X & A in X holds
union (rng f) in X
let f be Function; :: thesis: ( dom f = A & rng f c= X & A in X implies union (rng f) in X )
assume that
A2: dom f = A and
A3: rng f c= X and
A4: A in X ; :: thesis: union (rng f) in X
reconsider f9 = f as Function of A,X by A2, A3, FUNCT_2:2;
reconsider f9 = f9 as X -valued ManySortedSet of A ;
union (rng f9) in X by A4, A1;
hence union (rng f) in X ; :: thesis: verum

end;

hence X is FamUnion-closed ; :: thesis: verum

end;

assume A5: X is FamUnion-closed ; :: thesis: X is axiom_GU4

now :: thesis: for I being Element of X
for x being X -valued ManySortedSet of I holds union (rng x) in X

let I be Element of X; :: thesis: for x being X -valued ManySortedSet of I holds union (rng x) in X
let x be X -valued ManySortedSet of I; :: thesis: union (rng x) in X
dom x = I by PARTFUN1:def 2;
hence union (rng x) in X by A5; :: thesis: verum

end;

hence X is axiom_GU4 ; :: thesis: verum