let T be LATTICE; :: thesis: for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)
let A1, A2 be Subset of T; :: thesis: ( A1 is property(S) & A2 is property(S) implies A1 /\ A2 is property(S) )
assume that
A1: for D being non empty directed Subset of T st sup D in A1 holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A1 ) ) and
A2: for D being non empty directed Subset of T st sup D in A2 holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A2 ) ) ; :: according to WAYBEL11:def 3 :: thesis: A1 /\ A2 is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,T) in A1 /\ A2 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 A1 /\ A2 ) ) ) )
assume A3: sup D in A1 /\ A2 ; :: 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 A1 /\ A2 ) ) )
then sup D in A1 by XBOOLE_0:def 4;
then consider y1 being Element of T such that
A4: y1 in D and
A5: for x being Element of T st x in D & x >= y1 holds
x in A1 by A1;
sup D in A2 by A3, XBOOLE_0:def 4;
then consider y2 being Element of T such that
A6: y2 in D and
A7: for x being Element of T st x in D & x >= y2 holds
x in A2 by A2;
consider y being Element of T such that
A8: y in D and
A9: y1 <= y and
A10: y2 <= y by A4, A6, WAYBEL_0:def 1;
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 A1 /\ A2 ) ) )
thus y in D by A8; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in A1 /\ A2 )
let x be Element of T; :: thesis: ( not x in D or not y <= x or x in A1 /\ A2 )
assume that
A11: x in D and
A12: x >= y ; :: thesis: x in A1 /\ A2
A13: x in A2 by A12, A10, A7, A11, ORDERS_2:3;
x in A1 by A12, A9, A5, A11, ORDERS_2:3;
hence x in A1 /\ A2 by A13, XBOOLE_0:def 4; :: thesis: verum