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

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

hence
{ x where x is Element of L : V "/\" {x} c= V } is upper Subset of L
; :: thesis: verum
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, Th17, Th19;

hence y in G1 ; :: thesis: verum

end;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, Th17, Th19;

hence y in G1 ; :: thesis: verum