let L be non empty RelStr ; :: thesis: for S being upper Subset of L
for x being Element of L st x in S holds
uparrow x c= S
let S be upper Subset of L; :: thesis: for x being Element of L st x in S holds
uparrow x c= S
let x be Element of L; :: thesis: ( x in S implies uparrow x c= S )
assume A1: x in S ; :: thesis: uparrow x c= S
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in uparrow x or e in S )
assume A2: e in uparrow x ; :: thesis: e in S
then reconsider y = e as Element of L ;
x <= y by A2, WAYBEL_0:18;
hence e in S by A1, WAYBEL_0:def 20; :: thesis: verum