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

proof

let x, y be Element of ; :: 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 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 : V "/\" {x} c= V } is upper Subset of ; :: thesis: verum