let X be set ; :: thesis: for B1, B2 being Subset-Family of X st B1,B2 are_equivalent_generators holds
<.B1.] c= <.B2.]
let B1, B2 be Subset-Family of X; :: thesis: ( B1,B2 are_equivalent_generators implies <.B1.] c= <.B2.] )
assume A1: B1,B2 are_equivalent_generators ; :: thesis: <.B1.] c= <.B2.]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <.B1.] or x in <.B2.] )
assume A2: x in <.B1.] ; :: thesis: x in <.B2.]
then reconsider x0 = x as Subset of X ;
consider b1 being Element of B1 such that
A3: b1 c= x0 by A2, def3;
consider b2 being Element of B2 such that
A4: b2 c= b1 by A1;
b2 c= x0 by A3, A4;
hence x in <.B2.] by def3; :: thesis: verum