let T be LATTICE; :: thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A is property(S) ) holds
union F is property(S)
let F be Subset-Family of T; :: thesis: ( ( for A being Subset of T st A in F holds
A is property(S) ) implies union F is property(S) )
assume A1: for A being Subset of T st A in F holds
A is property(S) ; :: thesis: union F is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,T) in union F or ex b₁ being Element of the carrier of T st
( b₁ in D & ( for b₂ being Element of the carrier of T holds
( not b₂ in D or not b₁ <= b₂ or b₂ in union F ) ) ) )
assume sup D in union F ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in D & ( for b₂ being Element of the carrier of T holds
( not b₂ in D or not b₁ <= b₂ or b₂ in union F ) ) )
then consider A being set such that
A2: sup D in A and
A3: A in F by TARSKI:def 4;
reconsider A = A as Subset of T by A3;
A is property(S) by A1, A3;
then consider y being Element of T such that
A4: y in D and
A5: for x being Element of T st x in D & x >= y holds
x in A by A2;
take y ; :: thesis: ( y in D & ( for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in union F ) ) )
thus y in D by A4; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in union F )
let x be Element of T; :: thesis: ( not x in D or not y <= x or x in union F )
assume that
A6: x in D and
A7: x >= y ; :: thesis: x in union F
x in A by A6, A7, A5;
hence x in union F by A3, TARSKI:def 4; :: thesis: verum