let L be RelStr ; :: thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds

X is upper ) holds

union A is upper Subset of L

let A be Subset-Family of L; :: thesis: ( ( for X being Subset of L st X in A holds

X is upper ) implies union A is upper Subset of L )

assume A1: for X being Subset of L st X in A holds

X is upper ; :: thesis: union A is upper Subset of L

reconsider A = A as Subset-Family of L ;

reconsider X = union A as Subset of L ;

X is upper

X is upper ) holds

union A is upper Subset of L

let A be Subset-Family of L; :: thesis: ( ( for X being Subset of L st X in A holds

X is upper ) implies union A is upper Subset of L )

assume A1: for X being Subset of L st X in A holds

X is upper ; :: thesis: union A is upper Subset of L

reconsider A = A as Subset-Family of L ;

reconsider X = union A as Subset of L ;

X is upper

proof

hence
union A is upper Subset of L
; :: thesis: verum
let x, y be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( x in X & x <= y implies y in X )

assume x in X ; :: thesis: ( not x <= y 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 L by A3;

A4: Y is upper by A1, A3;

assume y >= x ; :: thesis: y in X

then y in Y by A2, A4;

hence y in X by A3, TARSKI:def 4; :: thesis: verum

end;assume x in X ; :: thesis: ( not x <= y 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 L by A3;

A4: Y is upper by A1, A3;

assume y >= x ; :: thesis: y in X

then y in Y by A2, A4;

hence y in X by A3, TARSKI:def 4; :: thesis: verum