let L be non empty 1-sorted ; :: thesis: for N being net of L
for X, Y being set st N is_eventually_in X & N is_eventually_in Y holds
X meets Y
let N be net of L; :: thesis: for X, Y being set st N is_eventually_in X & N is_eventually_in Y holds
X meets Y
let X, Y be set ; :: thesis: ( N is_eventually_in X & N is_eventually_in Y implies X meets Y )
assume N is_eventually_in X ; :: thesis: ( not N is_eventually_in Y or X meets Y )
then consider i1 being Element of N such that
A1: for j being Element of N st i1 <= j holds
N . j in X ;
assume N is_eventually_in Y ; :: thesis: X meets Y
then consider i2 being Element of N such that
A2: for j being Element of N st i2 <= j holds
N . j in Y ;
consider i being Element of N such that
A3: i1 <= i and
A4: i2 <= i by Def3;
A5: N . i in Y by A2, A4;
N . i in X by A1, A3;
hence X meets Y by A5, XBOOLE_0:3; :: thesis: verum