let L be non empty RelStr ; :: thesis: for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is Subset of L
let V be Subset of L; :: thesis: { x where x is Element of L : V "/\" {x} c= V } is Subset of L
set G = { x where x is Element of L : V "/\" {x} c= V } ;
{ x where x is Element of L : V "/\" {x} c= V } c= the carrier of L

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { x where x is Element of L : V "/\" {x} c= V } or q in the carrier of L )
assume q in { x where x is Element of L : V "/\" {x} c= V } ; :: thesis: q in the carrier of L
then ex x being Element of L st
( q = x & V "/\" {x} c= V ) ;
hence q in the carrier of L ; :: thesis: verum

end;

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