let V be non empty RLSStruct ; :: thesis: for A being Subset of V holds Int A c= conv A
let A be Subset of V; :: thesis: Int A c= conv A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Int A or x in conv A )
assume x in Int A ; :: thesis: x in conv A
hence x in conv A by Def1; :: thesis: verum