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

let x, y be Element of L; :: according to WAYBEL_0:def 19 :: thesis:
assume x in X ; :: thesis:
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 L by A3;
A4: Y is lower by A1, A3;
assume y <= x ; :: thesis:
then y in Y by A2, A4;
hence y in X by A3, TARSKI:def 4; :: thesis:

end;