let T be RelStr ; :: thesis: for A being upper Subset of T
for B being directed Subset of T holds A /\ B is directed
let A be upper Subset of T; :: thesis: for B being directed Subset of T holds A /\ B is directed
let B be directed Subset of T; :: thesis: A /\ B is directed
let x, y be Element of T; :: according to WAYBEL_0:def 1 :: thesis: ( not x in A /\ B or not y in A /\ B or ex b₁ being Element of the carrier of T st
( b₁ in A /\ B & x <= b₁ & y <= b₁ ) )
assume that
A1: x in A /\ B and
A2: y in A /\ B ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in A /\ B & x <= b₁ & y <= b₁ )
A3: x in B by A1, XBOOLE_0:def 4;
y in B by A2, XBOOLE_0:def 4;
then consider z being Element of T such that
A4: z in B and
A5: x <= z and
A6: y <= z by A3, WAYBEL_0:def 1;
take z ; :: thesis: ( z in A /\ B & x <= z & y <= z )
x in A by A1, XBOOLE_0:def 4;
then z in A by A5, WAYBEL_0:def 20;
hence z in A /\ B by A4, XBOOLE_0:def 4; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A5, A6; :: thesis: verum