let L be complete LATTICE; :: thesis: for x being Element of L holds (L -waybelow) -below x = waybelow x
let x be Element of L; :: thesis: (L -waybelow) -below x = waybelow x
set AR = L -waybelow ;
set A = { y where y is Element of L : [y,x] in L -waybelow } ;
set B = { y where y is Element of L : y << x } ;
A1: { y where y is Element of L : [y,x] in L -waybelow } c= { y where y is Element of L : y << x }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of L : [y,x] in L -waybelow } or a in { y where y is Element of L : y << x } )
assume a in { y where y is Element of L : [y,x] in L -waybelow } ; :: thesis: a in { y where y is Element of L : y << x }
then consider v being Element of L such that
A2: a = v and
A3: [v,x] in L -waybelow ;
v << x by A3, Def1;
hence a in { y where y is Element of L : y << x } by A2; :: thesis: verum

end;

{ y where y is Element of L : y << x } c= { y where y is Element of L : [y,x] in L -waybelow }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of L : y << x } or a in { y where y is Element of L : [y,x] in L -waybelow } )
assume a in { y where y is Element of L : y << x } ; :: thesis: a in { y where y is Element of L : [y,x] in L -waybelow }
then consider v being Element of L such that
A4: a = v and
A5: v << x ;
[v,x] in L -waybelow by A5, Def1;
hence a in { y where y is Element of L : [y,x] in L -waybelow } by A4; :: thesis: verum

end;

then { y where y is Element of L : [y,x] in L -waybelow } = { y where y is Element of L : y << x } by A1;
hence (L -waybelow) -below x = waybelow x by WAYBEL_3:def 3; :: thesis: verum