let L be RelStr ; :: thesis: for X, Y being Subset of L st X c= Y holds
downarrow X c= downarrow Y
let X, Y be Subset of L; :: thesis: ( X c= Y implies downarrow X c= downarrow Y )
assume A1: X c= Y ; :: thesis: downarrow X c= downarrow Y
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in downarrow X or q in downarrow Y )
assume A2: q in downarrow X ; :: thesis: q in downarrow Y
then reconsider x = q as Element of L ;
ex z being Element of L st
( x <= z & z in X ) by A2, WAYBEL_0:def 15;
hence q in downarrow Y by A1, WAYBEL_0:def 15; :: thesis: verum