let X be set ; :: thesis: for A, B being Subset-Family of X st A c= B holds
UniCl A c= UniCl B
let A, B be Subset-Family of X; :: thesis: ( A c= B implies UniCl A c= UniCl B )
assume A1: A c= B ; :: thesis: UniCl A c= UniCl B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl A or x in UniCl B )
assume A2: x in UniCl A ; :: thesis: x in UniCl B
then reconsider x' = x as Subset of X ;
consider T being Subset-Family of X such that
A3: ( T c= A & x' = union T ) by A2, Def1;
T c= B by A1, A3, XBOOLE_1:1;
hence x in UniCl B by A3, Def1; :: thesis: verum