let L be lower-bounded pseudocomplemented Lattice; :: thesis: for x being Element of L holds
( x in Skeleton L iff (x *) * = x )
let x be Element of L; :: thesis: ( x in Skeleton L iff (x *) * = x )

hereby :: thesis: ( (x *) * = x implies x in Skeleton L )

assume x in Skeleton L ; :: thesis: (x *) * = x
then consider a being Element of L such that
a1: x = a * ;
thus (x *) * = x by a1, Th7; :: thesis: verum

end;

assume (x *) * = x ; :: thesis: x in Skeleton L
hence x in Skeleton L ; :: thesis: verum