let N be antisymmetric with_infima RelStr ; :: thesis: for D, E being Subset of N
for X being upper Subset of N st D misses X holds
D "/\" E misses X
let D, E be Subset of N; :: thesis: for X being upper Subset of N st D misses X holds
D "/\" E misses X
let X be upper Subset of N; :: thesis: ( D misses X implies D "/\" E misses X )
assume A1: D /\ X = {} ; :: according to XBOOLE_0:def 7 :: thesis: D "/\" E misses X
assume (D "/\" E) /\ X <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider k being object such that
A2: k in (D "/\" E) /\ X by XBOOLE_0:def 1;
reconsider k = k as Element of N by A2;
A3: ( D "/\" E = { (d "/\" e) where d, e is Element of N : ( d in D & e in E ) } & k in D "/\" E ) by A2, XBOOLE_0:def 4, YELLOW_4:def 4;
A4: k in X by A2, XBOOLE_0:def 4;
consider d, e being Element of N such that
A5: k = d "/\" e and
A6: d in D and
e in E by A3;
d "/\" e <= d by YELLOW_0:23;
then d in X by A4, A5, WAYBEL_0:def 20;
hence contradiction by A1, A6, XBOOLE_0:def 4; :: thesis: verum