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

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

hence
{ x where x is Element of L : V "/\" {x} c= V } is Subset of L
; :: thesis: verum
let q be object ; :: 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;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