let L be non empty RelStr ; :: thesis: for S being non empty SubRelStr of L
for X being Subset of L
for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
let S be non empty SubRelStr of L; :: thesis: for X being Subset of L
for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
let X be Subset of L; :: thesis: for Y being Subset of S st X = Y holds
uparrow Y c= uparrow X
let Y be Subset of S; :: thesis: ( X = Y implies uparrow Y c= uparrow X )
assume A1: X = Y ; :: thesis: uparrow Y c= uparrow X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow Y or x in uparrow X )
assume A2: x in uparrow Y ; :: thesis: x in uparrow X
then reconsider x1 = x as Element of S ;
consider y1 being Element of S such that
A3: y1 <= x1 and
A4: y1 in Y by A2, WAYBEL_0:def 16;
reconsider x2 = x1, y2 = y1 as Element of L by YELLOW_0:58;
y2 <= x2 by A3, YELLOW_0:59;
hence x in uparrow X by A1, A4, WAYBEL_0:def 16; :: thesis: verum