let L be RelStr ; :: thesis: for A being Subset-Family of st ( for X being Subset of st X in A holds
X is lower ) holds
union A is lower Subset of
let A be Subset-Family of ; :: thesis: ( ( for X being Subset of st X in A holds
X is lower ) implies union A is lower Subset of )
assume A1: for X being Subset of st X in A holds
X is lower ; :: thesis: union A is lower Subset of
reconsider A = A as Subset-Family of ;
reconsider X = union A as Subset of ;
X is lower

proof

let x, y be Element of ; :: according to WAYBEL_0:def 19 :: thesis: ( x in X & y <= x implies y in X )
assume x in X ; :: thesis: ( not y <= x or y in X )
then consider Y being set such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
reconsider Y = Y as Subset of by A3;
A4: Y is lower by A1, A3;
assume y <= x ; :: thesis: y in X
then y in Y by A2, A4, Def19;
hence y in X by A3, TARSKI:def 4; :: thesis: verum

end;

hence union A is lower Subset of ; :: thesis: verum