let L be transitive antisymmetric with_infima RelStr ; :: thesis: for V being upper Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L
let V be upper Subset of L; :: thesis: { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L
reconsider G1 = { x where x is Element of L : V "/\" {x} c= V } as Subset of L by Lm2;
G1 is upper

proof

let x, y be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( not x in G1 or not x <= y or y in G1 )
assume x in G1 ; :: thesis: ( not x <= y or y in G1 )
then A1: ex x1 being Element of L st
( x1 = x & V "/\" {x1} c= V ) ;
assume x <= y ; :: thesis: y in G1
then V "/\" {y} c= V by A1, Th21, Th23;
hence y in G1 ; :: thesis: verum

end;

hence { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L ; :: thesis: verum