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