let L be antisymmetric with_infima RelStr ; :: thesis:
let X be upper Subset of L; :: thesis:
thus ( X is filtered implies for x, y being Element of L st x in X & y in X holds
x "/\" y in X ) :: thesis:

assume A1: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x >= z & y >= z ) ; :: according to WAYBEL_0:def 2 :: thesis:
let x, y be Element of L; :: thesis:
assume that
A2: x in X and
A3: y in X ; :: thesis:
consider z being Element of L such that
A4: z in X and
A5: x >= z and
A6: y >= z by A1, A2, A3;
x "/\" y >= z by A5, A6, YELLOW_0:23;
hence x "/\" y in X by A4, Def20; :: thesis:

end;